Data structure telling implicits of local variables is a map in the

intern_env

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

4 files changed, 14 insertions, 14 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e571803273..38492f88b5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -152,8 +152,8 @@ let build_newrecursive
         let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls))
-      (env0,[]) lnameargsardef in
+        (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
+      (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index feff5d67c6..4217b83faf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1410,7 +1410,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     interp_constr
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index aae5383892..640d3e60d6 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -26,11 +26,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=Constrintern.empty_internalization_env) 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=Constrintern.empty_internalization_env) 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 9098922e31..6fe31646ba 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -52,7 +52,7 @@ let evar_nf isevars c =
   Evarutil.nf_evar !isevars c
 
 let interp_gen kind isevars env
-               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+               ?(impls=Constrintern.empty_internalization_env) ?(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
@@ -61,13 +61,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=Constrintern.empty_internalization_env) c =
   interp_gen IsType isevars env ~impls c
 
-let interp_casted_constr isevars env ?(impls=[]) c typ =
+let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) 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=Constrintern.empty_internalization_env) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c
 
 let interp_open_constr isevars env c =
@@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       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
-    interp_casted_constr isevars ~impls:newimpls
-      (push_rel_context ctx env) body (lift 1 top_arity)
+    let newimpls = Idmap.singleton recname
+      (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
+       scopes @ [None]) in
+      interp_casted_constr isevars ~impls:newimpls
+	(push_rel_context ctx env) body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in