From cfadf920f60ae2977bd1f3c2bf0137f607c76467 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 21:12:51 +0000
Subject: Ajout d'un choix 'onlyparse'

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

(limited to 'interp')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index eef20a7b16..d24ac4673f 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,13 +31,14 @@ let _ = Summary.declare_summary
 let add_syntax_constant kn c =
   syntax_table := KNmap.add kn c !syntax_table
 
-let load_syntax_constant i ((sp,kn),c) =
+let load_syntax_constant i ((sp,kn),(c,onlyparse)) =
   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;
-  Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
+  if not onlyparse then
+    Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let open_syntax_constant i ((sp,kn),c) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
@@ -45,8 +46,8 @@ let open_syntax_constant i ((sp,kn),c) =
 let cache_syntax_constant d =
   load_syntax_constant 1 d
 
-let subst_syntax_constant ((sp,kn),subst,c) =
-  subst_aconstr subst c
+let subst_syntax_constant ((sp,kn),subst,(c,onlyparse)) =
+  (subst_aconstr subst c,onlyparse)
 
 let classify_syntax_constant (_,c) = Substitute c
 
@@ -59,8 +60,8 @@ let (in_syntax_constant, out_syntax_constant) =
     classify_function = classify_syntax_constant;
     export_function = (fun x -> Some x) } 
 
-let declare_syntactic_definition id c =
-  let _ = add_leaf id (in_syntax_constant c) in ()
+let declare_syntactic_definition id onlyparse c =
+  let _ = add_leaf id (in_syntax_constant (c,onlyparse)) in ()
 
 let rec set_loc loc _ a =
   map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index f4600d8dbf..87c3e75123 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,7 +16,7 @@ open Rawterm
 
 (* Syntactic definitions. *)
 
-val declare_syntactic_definition : identifier -> aconstr -> unit
+val declare_syntactic_definition : identifier -> bool -> aconstr -> unit
 
 val search_syntactic_definition : loc -> kernel_name -> rawconstr
 
-- 
cgit v1.2.3