From aadcf42183225553b8e5dcf49685ecb59459af58 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Nov 2002 16:17:38 +0000
Subject: Réaffichage des Syntactic Definition (printer constr_expr).
 Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et
 de l'affichage des délimiteurs de scopes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/syntax_def.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a49352da37..eef20a7b16 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,23 +31,20 @@ let _ = Summary.declare_summary
 let add_syntax_constant kn c =
   syntax_table := KNmap.add kn c !syntax_table
 
-let cache_syntax_constant ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
-
 let load_syntax_constant i ((sp,kn),c) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn
+  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let open_syntax_constant i ((sp,kn),c) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
 
+let cache_syntax_constant d =
+  load_syntax_constant 1 d
+
 let subst_syntax_constant ((sp,kn),subst,c) =
   subst_aconstr subst c
 
-- 
cgit v1.2.3