diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/API/API.mli b/API/API.mli index 92a515d5ce..0cfa3e328d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2556,6 +2556,20 @@ sig and closed_glob_constr = Glob_term.closed_glob_constr = { closure: closure; term: glob_constr } + + type var_map = Pattern.constr_under_binders Names.Id.Map.t + type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t + type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t + type ltac_var_map = Glob_term.ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Names.Id.t Names.Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) + } end module Libnames : @@ -2921,10 +2935,6 @@ sig | IsType | WithoutTypeConstraint - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr type inference_flags = Pretyping.inference_flags = { use_typeclasses : bool; @@ -2934,22 +2944,11 @@ sig expand_evars : bool } - type ltac_var_map = Pretyping.ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Names.Id.t Names.Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) - } type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = ltac_var_map * Glob_term.glob_constr + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr - val empty_lvar : ltac_var_map val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> ltac_var_map -> + Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> pure_open_constr val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr @@ -2963,11 +2962,11 @@ sig val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit val all_and_fail_flags : inference_flags val ise_pretype_gen : inference_flags -> Environ.env -> Evd.evar_map -> - ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Evarconv : @@ -3796,6 +3795,7 @@ sig val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern val map_glob_constr : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr + val empty_lvar : Glob_term.ltac_var_map end module Indrec : |