package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type glob_sign = Genintern.glob_sign = {
  1. ltacvars : Names.Id.Set.t;
  2. genv : Environ.env;
  3. extra : Genintern.Store.t;
}
val fully_empty_glob_sign : glob_sign
val make_empty_glob_sign : unit -> glob_sign
val intern_tactic_or_tacarg : glob_sign -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_hyp : glob_sign -> Names.lident -> Names.lident
val print_ltac : Libnames.qualid -> Pp.t
val dump_glob_red_expr : Tacexpr.raw_red_expr -> unit
val strict_check : bool ref
OCaml

Innovation. Community. Security.