Interp a definition with the implicit arguments of its local context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7

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) *)