Simplified the way internalization_data (i.e. bindings of bound vars

to their signature of implicit positions and scopes) is computed.
A bit of documentation in constrintern.mli.

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

3 files changed, 12 insertions, 13 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 2fe22364d..3c04dd9ca 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -27,11 +27,11 @@ open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
   SPretyping.understand_tcc_evars evdref env kind
     (intern_gen (kind=IsType) ~impls ( !evdref) env c)
 
-let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
 let interp_context_evars evdref env params =
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 0027cb1ff..634a6ea60 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -53,7 +53,7 @@ let evar_nf isevars c =
   Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
-               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
   let c' = SPretyping.understand_tcc_evars isevars env kind c' in
@@ -62,13 +62,13 @@ let interp_gen kind isevars env
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c
 
-let interp_type_evars isevars env ?(impls=([],[])) c =
+let interp_type_evars isevars env ?(impls=[]) c =
   interp_gen IsType isevars env ~impls c
 
-let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr isevars env ?(impls=[]) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
-let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
 let interp_open_constr isevars env c =
@@ -296,14 +296,13 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
     let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
-    let (r, l, impls, scopes) = 
+    let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
     in
     let newimpls = [(recname, (r, l, impls @ 
       [Some (id_of_string "recproof", Impargs.Manual, (true, false))], 
 			      scopes @ [None]))] in
-    let newimpls = Constrintern.set_internalization_env_params newimpls [] in
     interp_casted_constr isevars ~impls:newimpls
       (push_rel_context ctx env) body (lift 1 top_arity)
   in
@@ -442,8 +441,8 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Constrintern.compute_full_internalization_env env 
-    Constrintern.Recursive [] fixnames fixtypes fiximps 
+  let impls = Constrintern.compute_internalization_env env
+    Constrintern.Recursive fixnames fixtypes fiximps
   in
   let notations = List.flatten ntnl in
 
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 304aa139e..0f24915e3 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -13,7 +13,7 @@ val interp_gen :
   typing_constraint ->
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   ?allow_patvar:bool ->
   ?ltacvars:ltac_sign ->
   constr_expr -> constr
@@ -23,12 +23,12 @@ val interp_constr :
 val interp_type_evars :
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   constr_expr -> constr
 val interp_casted_constr_evars :
   evar_map ref ->
   env ->
-  ?impls:full_internalization_env ->
+  ?impls:internalization_env ->
   constr_expr -> types -> constr
 val interp_open_constr :
   evar_map ref -> env -> constr_expr -> constr