diff options
| author | herbelin | 2003-03-31 21:12:51 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-31 21:12:51 +0000 |
| commit | cfadf920f60ae2977bd1f3c2bf0137f607c76467 (patch) | |
| tree | 6888a225c88fcddb510b99247556a01be8d1f338 /interp | |
| parent | 24b97a16a839d896af0cbb291c12c70f9bcab448 (diff) | |
Ajout d'un choix 'onlyparse'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/syntax_def.ml | 13 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 2 |
2 files changed, 8 insertions, 7 deletions
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 |