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

1 files changed, 3 insertions, 3 deletions

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;