diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 39 |
1 files changed, 19 insertions, 20 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 7411fb84b..563230b59 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -7,17 +7,17 @@ (************************************************************************) open Names -open Constr open Evd open Environ +open Misctypes open Libnames open Globnames open Glob_term open Pattern +open EConstr open Constrexpr open Notation_term open Pretyping -open Misctypes (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) @@ -58,10 +58,10 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env -val compute_internalization_data : env -> var_internalization_type -> +val compute_internalization_data : env -> evar_map -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> +val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env @@ -78,11 +78,10 @@ val empty_ltac_sign : ltac_sign (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : env -> constr_expr -> glob_constr - -val intern_type : env -> constr_expr -> glob_constr +val intern_constr : env -> evar_map -> constr_expr -> glob_constr +val intern_type : env -> evar_map -> constr_expr -> glob_constr -val intern_gen : typing_constraint -> env -> +val intern_gen : typing_constraint -> env -> evar_map -> ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr @@ -100,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context + constr_expr -> types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -108,37 +107,37 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr + ?impls:internalization_env -> constr_expr -> evar_map * constr val interp_casted_constr_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr + ?impls:internalization_env -> constr_expr -> types -> evar_map * constr val interp_type_evars : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types + ?impls:internalization_env -> constr_expr -> evar_map * types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - evar_map * (EConstr.constr * Impargs.manual_implicits) + evar_map * (constr * Impargs.manual_implicits) val interp_casted_constr_evars_impls : env -> evar_map -> - ?impls:internalization_env -> constr_expr -> EConstr.types -> - evar_map * (EConstr.constr * Impargs.manual_implicits) + ?impls:internalization_env -> constr_expr -> types -> + evar_map * (constr * Impargs.manual_implicits) val interp_type_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - evar_map * (EConstr.types * Impargs.manual_implicits) + evar_map * (types * Impargs.manual_implicits) (** Interprets constr patterns *) val intern_constr_pattern : - env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) @@ -152,14 +151,14 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types +val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * types (** Interpret contexts: returns extended env and context *) val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map -> local_binder_expr list -> - evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)) + evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) |