package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type var_internalization_type =
  1. | Inductive of Names.Id.t list * bool
  2. | Recursive
  3. | Method
  4. | Variable
type var_internalization_data = var_internalization_type * Names.Id.t list * Impargs.implicit_status list * Notation_term.scope_name option list
type internalization_env = var_internalization_data Names.Id.Map.t
val empty_internalization_env : internalization_env
type ltac_sign = {
  1. ltac_vars : Names.Id.Set.t;
  2. ltac_bound : Names.Id.Set.t;
  3. ltac_extra : Genintern.Store.t;
}
val empty_ltac_sign : ltac_sign
val interp_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
val interp_casted_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * EConstr.constr
val interp_type_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.types
val interp_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)
val interp_casted_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)
val interp_type_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * (EConstr.types * Impargs.manual_implicits)
val intern_constr_pattern : Environ.env -> Evd.evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> Constrexpr.constr_pattern_expr -> Pattern.patvar list * Pattern.constr_pattern
val intern_reference : Libnames.qualid -> Names.GlobRef.t
val interp_reference : ltac_sign -> Libnames.qualid -> Glob_term.glob_constr
val interp_context_evars : ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int -> Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Evd.evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
val locate_reference : Libnames.qualid -> Names.GlobRef.t
val is_global : Names.Id.t -> bool
val parsing_explicit : bool ref
val for_grammar : ('a -> 'b) -> 'a -> 'b
val get_asymmetric_patterns : unit -> bool
val check_duplicate : ?loc:Loc.t -> (Libnames.qualid * Constrexpr.constr_expr) list -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct