diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 20 | ||||
| -rw-r--r-- | interp/constrintern.mli | 14 |
2 files changed, 17 insertions, 17 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 55e545edab..52765ff12d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1617,12 +1617,12 @@ let my_intern_constr sigma env lvar acc c = let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c -let intern_context global_level sigma env params = +let intern_context global_level sigma env impl_env params = let lvar = (([],[]), []) in - snd (List.fold_left + let lenv, bl = List.fold_left (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) ({ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = empty_internalization_env}, []) params) + tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl) let interp_rawcontext_gen understand_type understand_judgment env bl = let (env, par, _, impls) = @@ -1647,15 +1647,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params = - let bl = intern_context global_level sigma env params in - interp_rawcontext_gen understand_type understand_judgment env bl +let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = + let int_env,bl = intern_context global_level sigma env impl_env params in + int_env, interp_rawcontext_gen understand_type understand_judgment env bl -let interp_context ?(global_level=false) sigma env params = +let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~global_level sigma env params + (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params -let interp_context_evars ?(global_level=false) evdref env params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~global_level !evdref env params + (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 97b0f4fd1d..be78837ff3 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -82,7 +82,7 @@ val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list -val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list +val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list (** {6 Composing internalization with pretyping } *) @@ -152,14 +152,14 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types val interp_context_gen : (env -> glob_constr -> types) -> (env -> glob_constr -> unsafe_judgment) -> - ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits + ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context : ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits +val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits +val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) |