diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
| commit | aadcf42183225553b8e5dcf49685ecb59459af58 (patch) | |
| tree | 1ba2f2f69650f4cf1191bc16838a51b79795f228 /interp/syntax_def.ml | |
| parent | 22c9662db9caef7fbb3f51d89e17fb4aa3d52646 (diff) | |
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
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a49352da3..eef20a7b1 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 |