From c5de1d84957842c263fddaf7482087e7e0edfeb4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Mar 2001 12:38:22 +0000
Subject: La strategie de recherche de lookup_eliminator etait insuffisante

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1480 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/library/declare.ml b/library/declare.ml
index f7388133cf..9cd1041218 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -510,6 +510,13 @@ let declare_eliminations sp =
 (* Look up function for the default elimination constant *)
 
 let lookup_eliminator env path s =
-  let s = (string_of_id (basename path))^(elimination_suffix s) in
-  construct_reference env (kind_of_path path) (id_of_string s)
+  let dir, base,k = repr_path path in
+  let id = id_of_string ((string_of_id base)^(elimination_suffix s)) in
+  (* Try first to get an eliminator defined in the same section as the *)
+  (* inductive type *)
+  try construct_absolute_reference env (Names.make_path dir id k)
+  with Not_found ->
+  (* Then try to get a user-defined eliminator in some other places *)
+  (* using short name (e.g. for "eq_rec") *)
+  construct_reference env (kind_of_path path) id
   
-- 
cgit v1.2.3