From 146fb70f0729285fb4bb59613c73da0bad92d6c6 Mon Sep 17 00:00:00 2001
From: coq
Date: Tue, 24 Sep 2002 15:09:43 +0000
Subject: Un peu (plus) d'ordre dans Nametab...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0960c2fda9..bcb0b5499e 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -559,7 +559,7 @@ let lookup_eliminator ind_sp s =
   (* inductive type *)
   let ref = ConstRef (make_kn mp dp (label_of_id id)) in
   try 
-    let _ = full_name ref in
+    let _ = sp_of_global None ref in
       constr_of_reference ref
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
-- 
cgit v1.2.3