package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

type glob_sign = Genintern.glob_sign = {
  1. ltacvars : Names.Id.Set.t;
  2. genv : Environ.env;
  3. extra : Genintern.Store.t;
  4. intern_sign : Genintern.intern_variable_status;
}
val make_empty_glob_sign : unit -> glob_sign

build an empty glob_sign using Global.env() as environment

Main globalization functions

Low-level variants

val intern_tactic_or_tacarg : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_hyp : glob_sign -> Names.lident -> Names.lident

Adds a globalization function for extra generic arguments

Reduction expressions

val dump_glob_red_expr : Tacexpr.raw_red_expr -> unit
val strict_check : bool ref