From 85b4184369459fff82a11bd2708c10d77f10e9fd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Nov 2000 18:52:04 +0000
Subject: Prise en compte de noms absolus dans la nametab

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

(limited to 'pretyping')

diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 4801d017e7..1e63907a49 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -36,7 +36,7 @@ let (in_syntax_constant, out_syntax_constant) =
 let _ =
   cache_syntax_constant := fun (sp,c) ->
     add_syntax_constant sp c;
-    Nametab.push_object (basename sp) (sp, in_syntax_constant c)
+    Nametab.push_object sp (in_syntax_constant c)
 
 let declare_syntactic_definition id c =
   let _ = add_leaf id CCI (in_syntax_constant c) in ()
-- 
cgit v1.2.3