From 1d0e61fe25ffaec80bcc175df94797d8a9fdc868 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Jun 2010 11:53:55 +0000
Subject: 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
---
 plugins/funind/rawterm_to_relation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/rawterm_to_relation.ml')

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 ())
-- 
cgit v1.2.3