diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index bfccf03d1..b39f6e18b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -39,8 +39,8 @@ open Pretyping argument associates a list of implicit positions and scopes to identifiers declared in the [rel_context] of [env] *) -type var_internalisation_type = Inductive | Recursive | Method - +type var_internalisation_type = Inductive | Recursive | Method + type var_internalisation_data = var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list @@ -79,22 +79,22 @@ val interp_gen : typing_constraint -> evar_map -> env -> (* Particular instances *) -val interp_constr : evar_map -> env -> +val interp_constr : evar_map -> env -> constr_expr -> constr -val interp_type : evar_map -> env -> ?impls:full_implicits_env -> +val interp_type : evar_map -> env -> ?impls:full_implicits_env -> constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr -val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> +val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr (* Accepting evars and giving back the manual implicits in addition. *) -val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> +val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> @@ -105,7 +105,7 @@ val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> ?impls:full_implicits_env -> constr_expr -> constr * manual_implicits -val interp_casted_constr_evars : evar_defs ref -> env -> +val interp_casted_constr_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> @@ -117,8 +117,8 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment (* Interprets constr patterns *) -val intern_constr_pattern : - evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> +val intern_constr_pattern : + evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern val interp_reference : ltac_sign -> reference -> rawconstr @@ -131,10 +131,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types (* Interpret contexts: returns extended env and context *) -val interp_context : ?fail_anonymous:bool -> +val interp_context : ?fail_anonymous:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits -val interp_context_evars : ?fail_anonymous:bool -> +val interp_context_evars : ?fail_anonymous:bool -> evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) @@ -147,7 +147,7 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Interprets into a abbreviatable constr *) -val interp_aconstr : implicits_env -> identifier list * identifier list +val interp_aconstr : implicits_env -> identifier list * identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) |