Fixed commit 13125 (stricter check of induction args): an interpretation

checking function was used instead of a test of existence in the context.

Also restricted constr_of_id which had no reason to interpret a
posteriori an already interpreted identifier as a global
reference. Consequently adapted funind.

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

6 files changed, 10 insertions, 10 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bef89909de..361df3d1cf 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1009,7 +1009,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	  | _ -> ()
 
       in
-      Tacinterp.constr_of_id (pf_env g) equation_lemma_id
+      Constrintern.construct_reference (pf_hyps g) equation_lemma_id
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b756492b51..5ac5f9ce84 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -283,7 +283,7 @@ let change_property_sort toSort princ princName =
      compose_prod args (mkSort toSort)
     )
   in
-  let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in
+  let princName_as_constr = Constrintern.global_reference princName in
   let init =
     let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in
     mkApp(princName_as_constr,
@@ -688,7 +688,7 @@ let build_case_scheme fa =
   let env = Global.env ()
   and sigma = Evd.empty in
 (*   let id_to_constr id =  *)
-(*     Tacinterp.constr_of_id env  id *)
+(*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
 		 try Libnames.constr_of_global (Nametab.global f)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ccbabead3d..7ba1f71dc9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -232,7 +232,7 @@ let derive_inversion fix_names =
   try
     (* we first transform the fix_names identifier into their corresponding constant *)
     let fix_names_as_constant =
-      List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names
+      List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names
     in
     (*
        Then we check that the graphs have been defined
@@ -249,7 +249,7 @@ let derive_inversion fix_names =
 	  Ensures by : register_built
 	  i*)
 	(List.map
-	   (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+	   (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
 	   fix_names
 	)
     with e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 28de815ca0..080073cbc0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -84,7 +84,7 @@ let nf_zeta =
 (* [id_to_constr id] finds the term associated to [id] in the global environment *)
 let id_to_constr id =
   try
-    Tacinterp.constr_of_id (Global.env ())  id
+    Constrintern.global_reference id
   with Not_found ->
     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id))
 
@@ -797,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let finfo = find_Function_infos f_as_constant in
 	 update_Function
 	   {finfo with
-	      correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id)))
+	      correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id)))
 	   }
 
       )
@@ -849,7 +849,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let finfo = find_Function_infos f_as_constant in
 	 update_Function
 	   {finfo with
-	      completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id)))
+	      completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id)))
 	   }
       )
       funs;
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ccc37046f9..1cf74025ab 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -129,7 +129,7 @@ let prNamedRLDecl s lc =
   end
 
 let showind (id:identifier) =
-  let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+  let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
   List.iter (fun (nm, optcstr, tp) ->
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 3c3a36f037..5d282a5cb2 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1225,7 +1225,7 @@ let do_build_inductive
   let env =
     Array.fold_right
       (fun id env ->
-	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id))  env
+	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id))  env
       )
       funnames
       (Global.env ())