Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7

32 files changed, 1266 insertions, 801 deletions

diff --git a/.depend b/.depend
index e44966fc9..ed944c6af 100644
--- a/.depend
+++ b/.depend
@@ -1,6 +1,6 @@
 interp/constrextern.cmi: kernel/environ.cmi library/libnames.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi interp/symbols.cmi kernel/term.cmi \
     pretyping/termops.cmi interp/topconstr.cmi 
 interp/constrintern.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/impargs.cmi library/libnames.cmi \
@@ -429,16 +429,16 @@ interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
     kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \
-    kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \
-    kernel/univ.cmi lib/util.cmi interp/constrextern.cmi 
+    pretyping/rawterm.cmi kernel/sign.cmi interp/symbols.cmi kernel/term.cmi \
+    pretyping/termops.cmi interp/topconstr.cmi kernel/univ.cmi lib/util.cmi \
+    interp/constrextern.cmi 
 interp/constrextern.cmx: pretyping/classops.cmx library/declare.cmx \
     pretyping/detyping.cmx kernel/environ.cmx library/impargs.cmx \
     kernel/inductive.cmx library/libnames.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/rawterm.cmx pretyping/reductionops.cmx kernel/sign.cmx \
-    kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \
-    kernel/univ.cmx lib/util.cmx interp/constrextern.cmi 
+    pretyping/rawterm.cmx kernel/sign.cmx interp/symbols.cmx kernel/term.cmx \
+    pretyping/termops.cmx interp/topconstr.cmx kernel/univ.cmx lib/util.cmx \
+    interp/constrextern.cmi 
 interp/constrintern.cmo: library/declare.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi library/impargs.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
@@ -479,14 +479,16 @@ interp/ppextend.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
     interp/ppextend.cmi 
 interp/ppextend.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
     interp/ppextend.cmi 
-interp/symbols.cmo: lib/bignat.cmi library/lib.cmi library/libnames.cmi \
-    library/libobject.cmi kernel/names.cmi library/nametab.cmi \
-    lib/options.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
-    library/summary.cmi interp/topconstr.cmi lib/util.cmi interp/symbols.cmi 
-interp/symbols.cmx: lib/bignat.cmx library/lib.cmx library/libnames.cmx \
-    library/libobject.cmx kernel/names.cmx library/nametab.cmx \
-    lib/options.cmx lib/pp.cmx interp/ppextend.cmx pretyping/rawterm.cmx \
-    library/summary.cmx interp/topconstr.cmx lib/util.cmx interp/symbols.cmi 
+interp/symbols.cmo: lib/bignat.cmi lib/gmapl.cmi library/lib.cmi \
+    library/libnames.cmi library/libobject.cmi library/library.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
+    interp/ppextend.cmi pretyping/rawterm.cmi library/summary.cmi \
+    interp/topconstr.cmi lib/util.cmi interp/symbols.cmi 
+interp/symbols.cmx: lib/bignat.cmx lib/gmapl.cmx library/lib.cmx \
+    library/libnames.cmx library/libobject.cmx library/library.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
+    interp/ppextend.cmx pretyping/rawterm.cmx library/summary.cmx \
+    interp/topconstr.cmx lib/util.cmx interp/symbols.cmi 
 interp/syntax_def.cmo: library/lib.cmi library/libnames.cmi \
     library/libobject.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi library/summary.cmi interp/topconstr.cmi \
@@ -850,15 +852,15 @@ parsing/g_module.cmo: parsing/ast.cmi parsing/pcoq.cmi lib/pp.cmi \
 parsing/g_module.cmx: parsing/ast.cmx parsing/pcoq.cmx lib/pp.cmx \
     interp/topconstr.cmx lib/util.cmx 
 parsing/g_natsyntax.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
-    interp/coqlib.cmi parsing/esyntax.cmi parsing/extend.cmi \
-    library/libnames.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi interp/symbols.cmi parsing/termast.cmi \
-    lib/util.cmi parsing/g_natsyntax.cmi 
+    interp/coqlib.cmi parsing/esyntax.cmi library/libnames.cmi \
+    kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    interp/symbols.cmi parsing/termast.cmi lib/util.cmi \
+    parsing/g_natsyntax.cmi 
 parsing/g_natsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
-    interp/coqlib.cmx parsing/esyntax.cmx parsing/extend.cmx \
-    library/libnames.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \
-    lib/util.cmx parsing/g_natsyntax.cmi 
+    interp/coqlib.cmx parsing/esyntax.cmx library/libnames.cmx \
+    kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    interp/symbols.cmx parsing/termast.cmx lib/util.cmx \
+    parsing/g_natsyntax.cmi 
 parsing/g_prim.cmo: parsing/coqast.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi parsing/pcoq.cmi interp/topconstr.cmi 
 parsing/g_prim.cmx: parsing/coqast.cmx library/libnames.cmx kernel/names.cmx \
@@ -871,14 +873,14 @@ parsing/g_proofs.cmx: interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     toplevel/vernacexpr.cmx 
 parsing/g_rsyntax.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi parsing/extend.cmi library/libnames.cmi \
-    library/library.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi interp/symbols.cmi \
-    parsing/termast.cmi interp/topconstr.cmi lib/util.cmi 
+    kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \
+    lib/pp.cmi pretyping/rawterm.cmi interp/symbols.cmi parsing/termast.cmi \
+    interp/topconstr.cmi lib/util.cmi 
 parsing/g_rsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     parsing/esyntax.cmx parsing/extend.cmx library/libnames.cmx \
-    library/library.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx \
-    parsing/termast.cmx interp/topconstr.cmx lib/util.cmx 
+    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
+    lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \
+    interp/topconstr.cmx lib/util.cmx 
 parsing/g_tactic.cmo: parsing/ast.cmi interp/genarg.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
     interp/topconstr.cmi lib/util.cmi 
@@ -897,13 +899,13 @@ parsing/g_vernac.cmx: parsing/ast.cmx toplevel/class.cmx \
     toplevel/vernacexpr.cmx 
 parsing/g_zsyntax.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi parsing/extend.cmi library/libnames.cmi \
-    library/library.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi interp/symbols.cmi parsing/termast.cmi \
+    kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi interp/symbols.cmi parsing/termast.cmi \
     interp/topconstr.cmi lib/util.cmi parsing/g_zsyntax.cmi 
 parsing/g_zsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     parsing/esyntax.cmx parsing/extend.cmx library/libnames.cmx \
-    library/library.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \
-    lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \
+    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx interp/symbols.cmx parsing/termast.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/g_zsyntax.cmi 
 parsing/lexer.cmo: parsing/lexer.cmi 
 parsing/lexer.cmx: parsing/lexer.cmi 
@@ -917,17 +919,17 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \
     library/libnames.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
     lib/util.cmx parsing/pcoq.cmi 
-parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
-    lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \
-    kernel/term.cmi parsing/termast.cmi interp/topconstr.cmi lib/util.cmi \
+parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \
+    parsing/coqast.cmi lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
+    interp/symbols.cmi kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
     parsing/ppconstr.cmi 
-parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
-    lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \
-    kernel/term.cmx parsing/termast.cmx interp/topconstr.cmx lib/util.cmx \
+parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \
+    parsing/coqast.cmx lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx interp/ppextend.cmx pretyping/rawterm.cmx \
+    interp/symbols.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
     parsing/ppconstr.cmi 
 parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
@@ -957,20 +959,20 @@ parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     parsing/printmod.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
     kernel/sign.cmx interp/syntax_def.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
-parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi parsing/extend.cmi library/global.cmi \
-    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
-    parsing/ppconstr.cmi interp/ppextend.cmi kernel/sign.cmi kernel/term.cmi \
-    parsing/termast.cmi pretyping/termops.cmi lib/util.cmi \
-    parsing/printer.cmi 
-parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx parsing/extend.cmx library/global.cmx \
-    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
-    parsing/ppconstr.cmx interp/ppextend.cmx kernel/sign.cmx kernel/term.cmx \
-    parsing/termast.cmx pretyping/termops.cmx lib/util.cmx \
-    parsing/printer.cmi 
+parsing/printer.cmo: parsing/ast.cmi interp/constrextern.cmi \
+    parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
+    parsing/extend.cmi library/global.cmi library/libnames.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    pretyping/pattern.cmi lib/pp.cmi parsing/ppconstr.cmi interp/ppextend.cmi \
+    kernel/sign.cmi kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
+    lib/util.cmi parsing/printer.cmi 
+parsing/printer.cmx: parsing/ast.cmx interp/constrextern.cmx \
+    parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
+    parsing/extend.cmx library/global.cmx library/libnames.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    pretyping/pattern.cmx lib/pp.cmx parsing/ppconstr.cmx interp/ppextend.cmx \
+    kernel/sign.cmx kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
+    lib/util.cmx parsing/printer.cmi 
 parsing/printmod.cmo: kernel/declarations.cmi library/global.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/printmod.cmi 
@@ -1962,38 +1964,40 @@ toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
-    pretyping/classops.cmi toplevel/command.cmi interp/constrintern.cmi \
-    library/decl_kinds.cmo library/declaremods.cmi tactics/dhyp.cmi \
-    toplevel/discharge.cmi kernel/entries.cmi kernel/environ.cmi \
-    pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
-    library/goptions.cmi library/impargs.cmi pretyping/inductiveops.cmi \
-    library/lib.cmi library/libnames.cmi library/library.cmi \
-    toplevel/metasyntax.cmi toplevel/mltop.cmi interp/modintern.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi \
-    pretyping/pretyping.cmi parsing/printer.cmi parsing/printmod.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
-    toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
-    parsing/search.cmi library/states.cmi interp/symbols.cmi lib/system.cmi \
+    pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
+    interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
+    tactics/dhyp.cmi toplevel/discharge.cmi kernel/entries.cmi \
+    kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
+    library/global.cmi library/goptions.cmi library/impargs.cmi \
+    pretyping/inductiveops.cmi library/lib.cmi library/libnames.cmi \
+    library/library.cmi toplevel/metasyntax.cmi toplevel/mltop.cmi \
+    interp/modintern.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \
+    lib/pp_control.cmi parsing/prettyp.cmi pretyping/pretyping.cmi \
+    parsing/printer.cmi parsing/printmod.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi toplevel/record.cmi toplevel/recordobj.cmi \
+    proofs/refiner.cmi kernel/safe_typing.cmi parsing/search.cmi \
+    library/states.cmi interp/symbols.cmi lib/system.cmi \
     tactics/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
     proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \
     parsing/termast.cmi interp/topconstr.cmi kernel/typeops.cmi \
     kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \
     toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: tactics/auto.cmx toplevel/class.cmx \
-    pretyping/classops.cmx toplevel/command.cmx interp/constrintern.cmx \
-    library/decl_kinds.cmx library/declaremods.cmx tactics/dhyp.cmx \
-    toplevel/discharge.cmx kernel/entries.cmx kernel/environ.cmx \
-    pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
-    library/goptions.cmx library/impargs.cmx pretyping/inductiveops.cmx \
-    library/lib.cmx library/libnames.cmx library/library.cmx \
-    toplevel/metasyntax.cmx toplevel/mltop.cmx interp/modintern.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx \
-    pretyping/pretyping.cmx parsing/printer.cmx parsing/printmod.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
-    toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
-    parsing/search.cmx library/states.cmx interp/symbols.cmx lib/system.cmx \
+    pretyping/classops.cmx toplevel/command.cmx interp/constrextern.cmx \
+    interp/constrintern.cmx library/decl_kinds.cmx library/declaremods.cmx \
+    tactics/dhyp.cmx toplevel/discharge.cmx kernel/entries.cmx \
+    kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
+    library/global.cmx library/goptions.cmx library/impargs.cmx \
+    pretyping/inductiveops.cmx library/lib.cmx library/libnames.cmx \
+    library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmx \
+    interp/modintern.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \
+    lib/pp_control.cmx parsing/prettyp.cmx pretyping/pretyping.cmx \
+    parsing/printer.cmx parsing/printmod.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx toplevel/record.cmx toplevel/recordobj.cmx \
+    proofs/refiner.cmx kernel/safe_typing.cmx parsing/search.cmx \
+    library/states.cmx interp/symbols.cmx lib/system.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \
     parsing/termast.cmx interp/topconstr.cmx kernel/typeops.cmx \
diff --git a/.depend.coq b/.depend.coq
index 8be4567ff..6f6be0579 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -5,7 +5,7 @@ theories/Init/PeanoSyntax.vo: theories/Init/PeanoSyntax.v theories/Init/Datatype
 theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
 theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
-theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/Datatypes.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo
+theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/DatatypesSyntax.vo theories/Init/Specif.vo
 theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
diff --git a/CHANGES b/CHANGES
index 5be095ab8..e3393dc6e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,8 @@ Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
   set a notation sets has been developped for nat, Z and R
+- New command "Notation" for declaring notations simultaneously for
+  parsing and printing
 - Declarations with only implicit arguments now handled (e.g. the
   argument of nil can be set implicit; use !nil to refer to nil
   without arguments)
@@ -25,6 +27,10 @@ Library
 - Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
   (lt_wf_rec, ...) are now transparent. This may be source of
   incompatibilities.
+- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
+  ProjS1, ProjS2, Error, Value and Except are turned to
+  notations. They now must be applied (incompatibilities only in
+  unrealistic cases).
 
 Language
 
@@ -74,10 +80,13 @@ Tactics
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
+- New syntax for Ring and Field when arguments are provided (use "Ring on" and
+  "Field on")
 
 Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print
+- "Print Term id" is an alias for "Print id"
 
 Incompatibilities
 
diff --git a/Makefile b/Makefile
index 2c492ed75..5bdbe1043 100644
--- a/Makefile
+++ b/Makefile
@@ -230,7 +230,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
   interp/constrintern.cmo interp/coqlib.cmo \
   parsing/pcoq.cmo parsing/ast.cmo \
   parsing/extend.cmo pretyping/detyping.cmo \
-  parsing/termast.cmo interp/modintern.cmo \
+  parsing/termast.cmo interp/modintern.cmo interp/constrextern.cmo\
   parsing/g_prim.cmo parsing/g_basevernac.cmo \
   parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \
   parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6bcc2433d..57e7189a7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1789,7 +1789,8 @@ let xlate_vernac =
 	| PrintLocalContext -> xlate_error "TODO: Print"
 	| PrintTables -> xlate_error "TODO: Print Tables"
         | PrintModuleType _ -> xlate_error "TODO: Print Module Type"
-        | PrintModule _ -> xlate_error "TODO: Print Module")
+        | PrintModule _ -> xlate_error "TODO: Print Module"
+        | PrintScope _ -> xlate_error "TODO: Print Scope")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment id -> CT_section_end (xlate_ident id)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ae4c2214..c813cf71d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -39,9 +39,6 @@ let print_arguments = ref false
 (* If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
 
-(* This forces printing of cast nodes *)
-let print_casts = ref true
-
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
@@ -56,6 +53,8 @@ let print_coercions = ref false
 (* This forces printing universe names of Type{.} *)
 let print_universes = ref false
 
+(* This suppresses printing of numeral and symbols *)
+let print_no_symbol = ref false
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -63,10 +62,23 @@ let with_option o f x =
   with e -> o := old; raise e
 
 let with_arguments f = with_option print_arguments f
-let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
 let with_universes f = with_option print_universes f
+let without_symbols f = with_option print_no_symbol f
+
+(**********************************************************************)
+(* Various externalisation functions *)
+
+let insert_delimiters e = function
+  | None -> e
+  | Some sc -> CDelimiters (dummy_loc,sc,e)
+
+let insert_pat_delimiters e = function
+  | None -> e
+  | Some sc -> CPatDelimiters (dummy_loc,sc,e)
+
+let loc = dummy_loc (* shorter... *)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -90,13 +102,21 @@ let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
 let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r)
 
 (**********************************************************************)
-(* conversion of patterns                                             *)
-
-let rec extern_cases_pattern = function   (* loc is thrown away for printing *)
-  | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
-  | PatVar (loc,Anonymous) -> CPatAtom (loc, None) 
-  | PatCstr(loc,cstrsp,args,na) ->
-      let args = List.map extern_cases_pattern args in
+(* conversion of terms and cases patterns                             *)
+
+let rec extern_cases_pattern_in_scope scopes pat =
+  try 
+    if !print_no_symbol then raise No_match;
+    let (sc,n) = Symbols.uninterp_cases_numeral pat in
+    match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_pat_delimiters (CPatNumeral (loc,n)) scopt
+  with No_match ->
+  match pat with
+  | PatVar (_,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
+  | PatVar (_,Anonymous) -> CPatAtom (loc, None) 
+  | PatCstr(_,cstrsp,args,na) ->
+      let args = List.map (extern_cases_pattern_in_scope scopes) args in
       let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in
       (match na with
 	| Name id -> CPatAlias (loc,p,id)
@@ -140,14 +160,31 @@ let rec skip_coercion dest_ref (f,args as app) =
     with Not_found -> app
 
 let extern_app impl f args =
-  if !print_implicits & not !print_implicits_explicit_args then 
+  if (!print_implicits & not !print_implicits_explicit_args) then 
     CAppExpl (dummy_loc, f, args)
   else
     explicitize impl (CRef f) args
 
-let loc = dummy_loc
+let rec extern_args extern scopes args subscopes =
+  match args with
+    | [] -> []
+    | a::args ->
+	let argscopes, subscopes = match subscopes with
+	  | [] -> scopes, []
+	  | scopt::subscopes -> option_cons scopt scopes, subscopes in
+	extern argscopes a :: extern_args extern scopes args subscopes
+
+let rec extern scopes r =
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_numeral scopes r (Symbols.uninterp_numeral r)
+  with No_match ->
+
+  try 
+    if !print_no_symbol then raise No_match;
+    extern_symbol scopes r (Symbols.uninterp_notations r)
+  with No_match -> match r with
 
-let rec extern = function
   | RRef (_,ref) -> CRef (extern_ref ref)
 
   | RVar (_,id) -> CRef (Ident (loc,id))
@@ -159,51 +196,55 @@ let rec extern = function
   | RApp (_,f,args) ->
       let (f,args) =
 	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
-      let args = List.map extern args in
       (match f with
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
 	 | RRef (loc,ref) ->
+	     let subscopes = Symbols.find_arguments_scope ref in
+	     let args = extern_args extern scopes args subscopes in
 	     extern_app (implicits_of_global ref) (extern_ref ref) args
-	 | _       -> explicitize [] (extern f) args)
+	 | _       -> 
+	     explicitize [] (extern scopes f) (List.map (extern scopes) args))
 
   | RProd (_,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
-      CArrow (loc,extern t,extern c)
+      CArrow (loc,extern scopes t,extern scopes c)
 
   | RLetIn (_,na,t,c) ->
-      CLetIn (loc,(loc,na),extern t,extern c)
+      CLetIn (loc,(loc,na),extern scopes t,extern scopes c)
 
   | RProd (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_prod t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_prod scopes t c in
       CProdN (loc,[(loc,na)::idl,t],c)
 
   | RLambda (_,na,t,c) ->
-      let t = extern t in
-      let (idl,c) = factorize_lambda t c in
+      let t = extern scopes t in
+      let (idl,c) = factorize_lambda scopes t c in
       CLambdaN (loc,[(loc,na)::idl,t],c)
 
   | RCases (_,typopt,tml,eqns) ->
-      let pred = option_app extern typopt in
-      let tml = List.map extern tml in
-      let eqns = List.map extern_eqn eqns in 
+      let pred = option_app (extern scopes) typopt in
+      let tml = List.map (extern scopes) tml in
+      let eqns = List.map (extern_eqn scopes) eqns in 
       CCases (loc,pred,tml,eqns)
 	
   | ROrderedCase (_,cs,typopt,tm,bv) ->
-      let bv = Array.to_list (Array.map extern bv) in
-      COrderedCase (loc,cs,option_app extern typopt,extern tm,bv)
+      let bv = Array.to_list (Array.map (extern scopes) bv) in
+      COrderedCase
+	(loc,cs,option_app (extern scopes) typopt,extern scopes tm,bv)
 
   | RRec (_,fk,idv,tyv,bv) ->
       (match fk with
 	 | RFix (nv,n) ->
 	     let listdecl = 
-	       Array.mapi
-		 (fun i fi -> (fi,nv.(i),extern tyv.(i),extern bv.(i))) idv
+	       Array.mapi (fun i fi ->
+		 (fi,nv.(i),extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
 	     let listdecl =
-               Array.mapi (fun i fi -> (fi,extern tyv.(i),extern bv.(i))) idv
+               Array.mapi (fun i fi ->
+		 (fi,extern scopes tyv.(i),extern scopes bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
@@ -216,46 +257,71 @@ let rec extern = function
 
   | RHole (_,e) -> CHole loc
 
-  | RCast (_,c,t) -> CCast (loc,extern c,extern t)
+  | RCast (_,c,t) -> CCast (loc,extern scopes c,extern scopes t)
 
   | RDynamic (_,d) -> CDynamic (loc,d)
 	
-and factorize_prod aty = function
+and factorize_prod scopes aty = function
   | RProd (_,Name id,ty,c)
-      when aty = extern ty
-	& not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
-	-> let (nal,c) = factorize_prod aty c in ((loc,Name id)::nal,c)
-  | c -> ([],extern c)
+      when aty = extern scopes ty
+	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
+	-> let (nal,c) = factorize_prod scopes aty c in ((loc,Name id)::nal,c)
+  | c -> ([],extern scopes c)
 
-and factorize_lambda aty = function
+and factorize_lambda scopes aty = function
   | RLambda (_,na,ty,c)
-      when aty = extern ty
+      when aty = extern scopes ty
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-	-> let (nal,c) = factorize_lambda aty c in ((loc,na)::nal,c)
-  | c -> ([],extern c)
-
-and extern_eqn (loc,ids,pl,c) =
-  (loc,List.map extern_cases_pattern pl,extern c)
-(*
-and extern_numerals r =
-  on_numeral (fun p ->
-    match filter p r with
-      | Some f 
-
-and extern_symbols r =
-*)
-
-let extern_rawconstr = extern
+	-> let (nal,c) = factorize_lambda scopes aty c in ((loc,na)::nal,c)
+  | c -> ([],extern scopes c)
+
+and extern_eqn scopes (loc,ids,pl,c) =
+  (loc,List.map (extern_cases_pattern_in_scope scopes) pl,extern scopes c)
+
+and extern_numeral scopes t (sc,n) =
+  match Symbols.availability_of_numeral sc scopes with
+    | None -> raise No_match
+    | Some scopt -> insert_delimiters (CNumeral (loc,n)) scopt
+
+and extern_symbol scopes t = function
+  | [] -> raise No_match
+  | (sc,ntn,pat,n as rule)::rules ->
+      try
+	(* Adjusts to the number of arguments expected by the notation *)
+	let (t,args) = match t,n with
+	  | RApp (_,f,args), Some n when List.length args > n ->
+	      let args1, args2 = list_chop n args in
+	      RApp (loc,f,args1), args2
+	  | _ -> t,[] in
+	(* Try matching ... *)
+	let subst = match_aconstr t pat in
+	(* Try availability of interpretation ... *)
+	(match Symbols.availability_of_notation (sc,ntn) scopes with
+          (* Uninterpretation is not allowed in current context *)
+	  | None -> raise No_match
+          (* Uninterpretation is allowed in current context *)
+	  | Some scopt ->
+	      let scopes = option_cons scopt scopes in
+	      let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in
+	      let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in
+	      if args = [] then e 
+	      else explicitize [] e (List.map (extern scopes) args))
+      with
+	  No_match -> extern_symbol scopes t rules
+
+let extern_rawconstr = 
+  extern (Symbols.current_scopes())
+
+let extern_cases_pattern = 
+  extern_cases_pattern_in_scope (Symbols.current_scopes())
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
        
 let extern_constr at_top env t =
-  let t' =
-    if !print_casts then t
-    else Reductionops.local_strong strip_outer_cast t in
   let avoid = if at_top then ids_of_context env else [] in
-  extern (Detyping.detype env avoid (names_of_rel_context env) t')
+  extern (Symbols.current_scopes())
+    (Detyping.detype env avoid (names_of_rel_context env) t)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -319,9 +385,12 @@ let rec extern_pattern tenv env = function
 	(loc,cs,option_app (extern_pattern tenv env) typopt,
 	 extern_pattern tenv env tm,bv)
 
-  | PFix f -> extern (Detyping.detype tenv [] env (mkFix f))
+  | PFix f ->
+      extern (Symbols.current_scopes()) (Detyping.detype tenv [] env (mkFix f))
 
-  | PCoFix c -> extern (Detyping.detype tenv [] env (mkCoFix c))
+  | PCoFix c ->
+      extern (Symbols.current_scopes())
+        (Detyping.detype tenv [] env (mkCoFix c))
 
   | PSort s ->
       let s = match s with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index cfa00c006..614cbfdd4 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -19,6 +19,7 @@ open Nametab
 open Rawterm
 open Pattern
 open Topconstr
+open Symbols
 (*i*)
 
 (* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -36,14 +37,23 @@ val extern_ref    : global_reference -> reference
 
 (* For debugging *)
 val print_implicits : bool ref
-val print_casts : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
 val print_universes : bool ref
 
-val with_casts : ('a -> 'b) -> 'a -> 'b
+(* This governs printing of implicit arguments. If [with_implicits] is
+   on and not [with_arguments] then implicit args are printed prefixed
+   by "!"; if [with_implicits] and [with_arguments] are both on the
+   function and not the arguments is prefixed by "!" *)
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing of coercions *)
 val with_coercions : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing universe names of Type{.} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
+
+(* This suppresses printing of numeral and symbols *)
+val without_symbols : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e760f3e92..7236335c3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -117,23 +117,21 @@ let add_glob loc ref =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-(* Is it a bound variables? *)
 let intern_var (env,impls,_) (vars1,vars2) loc id =
+  (* Is [id] bound in  *)
+  if Idset.mem id env or List.mem id vars1
+  then
+    RVar (loc,id), (try List.assoc id impls with Not_found -> []), []
+  else
+  (* Is [id] a section variable *)
+  let _ = Sign.lookup_named id vars2 in
+  (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
   let imps, args_scopes =
-    (* Is [id] bound in  *)
-    if Idset.mem id env or List.mem id vars1
-    then
-      try List.assoc id impls, []
-      with Not_found -> [], []
-    else
-    (* Is [id] a section variable *)
-    let _ = Sign.lookup_named id vars2 in
-    (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
     try
       let ref = VarRef id in
       implicits_of_global ref, find_arguments_scope ref
-    with _ -> [], []
-  in RVar (loc, id), imps, args_scopes
+    with _ -> [], [] in
+  RRef (loc, VarRef id), imps, args_scopes
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid env vars loc qid =
@@ -334,11 +332,8 @@ let coerce_to_id = function
         str"This expression should be a simple identifier")
 
 let traverse_binder id (subst,(ids,impls,scopes as env)) =
-  try 
-    let id' = coerce_to_id (List.assoc id subst) in
-    id', (subst,(Idset.add id' ids,impls,scopes))
-  with Not_found ->
-    id, (List.remove_assoc id subst,env)
+  let id = try coerce_to_id (List.assoc id subst) with Not_found -> id in
+  id,(subst,(Idset.add id ids,impls,scopes))
 
 let rec subst_rawconstr loc interp (subst,env as senv) = function
   | AVar id ->
diff --git a/interp/symbols.ml b/interp/symbols.ml
index c6eff9ab9..87282f046 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -14,6 +14,7 @@ open Pp
 open Bignat
 open Names
 open Nametab
+open Libnames
 open Summary
 open Rawterm
 open Topconstr
@@ -41,7 +42,7 @@ open Ppextend
 type level = precedence * precedence list
 type delimiters = string * string
 type scope = {
-  notations: (aconstr * level) Stringmap.t;
+  notations: (aconstr * (level * string)) Stringmap.t;
   delimiters: delimiters option
 }
 type scopes = scope_name list
@@ -58,6 +59,9 @@ let default_scope = "core_scope"
 
 let _ = Stringmap.add default_scope empty_scope !scope_map
 
+(**********************************************************************)
+(* The global stack of scopes                                         *)
+
 let scope_stack = ref [default_scope]
 
 let current_scopes () = !scope_stack
@@ -65,26 +69,8 @@ let current_scopes () = !scope_stack
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
 (**********************************************************************)
-(* Interpreting numbers (not in summary because functional objects)   *)
-
-type numeral_interpreter_name = string
-type numeral_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
-
-let numeral_interpreter_tab =
-  (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t)
-
-let declare_numeral_interpreter sc t =
-  Hashtbl.add numeral_interpreter_tab sc t
-
-let lookup_numeral_interpreter s =
-  try 
-    Hashtbl.find numeral_interpreter_tab s
-  with Not_found -> 
-    error ("No interpretation for numerals in scope "^s)
+(* Operations on scopes *)
 
-(* For loading without opening *)
 let declare_scope scope =
   try let _ = Stringmap.find scope !scope_map in ()
   with Not_found ->
@@ -97,6 +83,9 @@ let find_scope scope =
 
 let check_scope sc = let _ = find_scope sc in ()
 
+(**********************************************************************)
+(* Delimiters *)
+
 let declare_delimiters scope dlm =
   let sc = find_scope scope in
   if sc.delimiters <> None && Options.is_verbose () then
@@ -104,105 +93,147 @@ let declare_delimiters scope dlm =
   let sc = { sc with delimiters = Some dlm } in
   scope_map := Stringmap.add scope sc !scope_map   
 
-(* The mapping between notations and production *)
+let find_delimiters scope = (find_scope scope).delimiters
 
-let declare_notation nt scope (c,prec as info) =
-  let sc = find_scope scope in
-  if Stringmap.mem nt sc.notations && Options.is_verbose () then
-    warning ("Notation "^nt^" is already used in scope "^scope);
-  let sc = { sc with notations = Stringmap.add nt info sc.notations } in
-  scope_map := Stringmap.add scope sc !scope_map
+(* Uninterpretation tables *)
 
-let rec find_interpretation f = function
-  | scope::scopes ->
-      (try f (find_scope scope)
-       with Not_found -> find_interpretation f scopes)
-  | [] -> raise Not_found
+type interpretation = identifier list * aconstr
+type interp_rule = scope_name * notation * interpretation * int option
 
-let rec interp_notation ntn scopes =
-  let f scope = fst (Stringmap.find ntn scope.notations) in
-  try find_interpretation f scopes
-  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+(* We define keys for rawterm and aconstr to split the syntax entries
+   according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
-let find_notation_with_delimiters scope =
-  match (Stringmap.find scope !scope_map).delimiters with
-    | Some dlm -> Some (Some dlm)
-    | None -> None
+type key =
+  | RefKey of global_reference
+  | Oth
 
-let rec find_notation_without_delimiters ntn_scope ntn = function
-  | scope::scopes ->
-      (* Is the expected printer attached to the most recently open scope? *)
-      if scope = ntn_scope then
-	Some None
-      else
-	(* If the most recently open scope has a printer for this pattern
-    	   but not the expected one then we need delimiters *)
-	if Stringmap.mem ntn (Stringmap.find scope !scope_map).notations then
-	  find_notation_with_delimiters ntn_scope
-	else
-	  find_notation_without_delimiters ntn_scope ntn scopes
-  | [] ->
-      find_notation_with_delimiters ntn_scope
+(* Scopes table : interpretation -> scope_name *)
+let notations_key_table = ref Gmapl.empty
+let numeral_key_table = Hashtbl.create 7
 
-let find_notation ntn_scope ntn scopes =
-  match 
-    find_notation_without_delimiters ntn_scope ntn scopes
-  with
-    | None -> None
-    | Some None -> Some (None,scopes)
-    | Some x -> Some (x,ntn_scope::scopes)
+let rawconstr_key = function
+  | RApp (_,RRef (_,ref),_) -> RefKey ref
+  | RRef (_,ref) -> RefKey ref
+  | _ -> Oth
 
-let exists_notation_in_scope scope prec ntn r =
-  try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = (r,prec)
-  with Not_found -> false
+let aconstr_key = function
+  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
+  | ARef ref -> RefKey ref, Some 0
+  | _ -> Oth, None
 
-let exists_notation_prec prec nt sc =
-  try snd (Stringmap.find nt sc.notations) = prec with Not_found -> false
+let pattern_key = function
+  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
+  | _ -> Oth
 
-let exists_notation prec nt =
-  Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc)
-    !scope_map false 
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects)   *)
 
-(* We have to print delimiters; look for the more recent defined one *)
-(* Do we need to print delimiters? To know it, we look for a numeral *)
-(* printer available in the current stack of scopes *)
-let find_numeral_with_delimiters scope =
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
+
+type required_module = string list 
+
+let numeral_interpreter_tab =
+  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_scope sc;
+  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
+  List.iter
+    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
+      (sc,uninterp,uninterpc))
+    patl
+
+let check_required_module loc sc d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_loaded dir) then
+    user_err_loc (loc,"numeral_interpreter",
+    str ("Cannot interpret numbers in "^sc^" without requiring first module "
+    ^(list_last d)))
+
+let lookup_numeral_interpreter loc sc =
+  try
+    let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
+    check_required_module loc sc dir;
+    interpreter
+  with Not_found -> 
+    error ("No interpretation for numerals in scope "^sc)
+
+(* Look if some notation or numeral printer in [scope] can be used in
+   the scope stack [scopes], and if yes, using delimiters or not *)
+
+let find_with_delimiters scope =
   match (Stringmap.find scope !scope_map).delimiters with
-    | Some dlm -> Some (Some dlm)
+    | Some _ -> Some (Some scope)
     | None -> None
 
-let rec find_numeral_without_delimiters printer_scope = function
+let rec find_without_delimiters find ntn_scope = function
   | scope :: scopes -> 
-      (* Is the expected printer attached to the most recently open scope? *)
-      if scope = printer_scope then
+      (* Is the expected ntn/numpr attached to the most recently open scope? *)
+      if scope = ntn_scope then
 	Some None
       else
-	(* If the most recently open scope has a printer for numerals
+	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
-	if not (Hashtbl.mem numeral_interpreter_tab scope) then
-	  find_numeral_without_delimiters printer_scope scopes
+	if find scope then
+	  find_with_delimiters ntn_scope
 	else
-	  find_numeral_with_delimiters printer_scope
+	  find_without_delimiters find ntn_scope scopes
   | [] ->
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
-      find_numeral_with_delimiters printer_scope
+      find_with_delimiters ntn_scope
+
+(* The mapping between notations and their interpretation *)
+
+let declare_interpretation ntn scope pat =
+  let sc = find_scope scope in
+  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+    warning ("Notation "^ntn^" is already used in scope "^scope);
+  let sc = { sc with notations = Stringmap.add ntn pat sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map
+
+let declare_uninterpretation ntn scope metas c =
+  let (key,n) = aconstr_key c in
+  notations_key_table :=
+    Gmapl.add key (scope,ntn,(metas,c),n) !notations_key_table
 
-let find_numeral_printer printer_scope scopes =
+let declare_notation ntn scope (metas,c) prec df onlyparse =
+  declare_interpretation ntn scope (c,(prec,df));
+  if not onlyparse then declare_uninterpretation ntn scope metas c
+
+let rec find_interpretation f = function
+  | scope::scopes ->
+      (try f (find_scope scope)
+       with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation ntn scopes =
+  let f scope = fst (Stringmap.find ntn scope.notations) in
+  try find_interpretation f scopes
+  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+
+let uninterp_notations c =
+  Gmapl.find (rawconstr_key c) !notations_key_table
+
+let availability_of_notation (ntn_scope,ntn) scopes =
   match 
-    find_numeral_without_delimiters printer_scope scopes
+    let f scope =
+      Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+    find_without_delimiters f ntn_scope scopes
   with
     | None -> None
-    | Some None -> Some (None,scopes)
-    | Some x -> Some (x,printer_scope::scopes)
-
-(* This is the map associating the scope a numeral printer belongs to *)
-(*
-let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t)
-*)
+    | Some None -> Some None
+    | Some (Some dlm) -> Some (Some ntn_scope)
 
 let rec interp_numeral loc n = function
   | scope :: scopes ->
-      (try fst (lookup_numeral_interpreter scope) loc n
+      (try fst (lookup_numeral_interpreter loc scope) loc n
        with Not_found -> interp_numeral loc n scopes)
   | [] ->
       user_err_loc (loc,"interp_numeral",
@@ -211,7 +242,7 @@ let rec interp_numeral loc n = function
 let rec interp_numeral_as_pattern loc n name = function
   | scope :: scopes ->
       (try 
-	match snd (lookup_numeral_interpreter scope) with
+	match snd (lookup_numeral_interpreter loc scope) with
 	  | None -> raise Not_found
 	  | Some g -> g loc n name
 	with Not_found -> interp_numeral_as_pattern loc n name scopes)
@@ -219,6 +250,48 @@ let rec interp_numeral_as_pattern loc n name = function
       user_err_loc (loc,"interp_numeral_as_pattern",
       str "No interpretation for numeral " ++ pr_bigint n)
 
+let uninterp_numeral c =
+  try 
+    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+    match numpr c with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let uninterp_cases_numeral c =
+  try 
+    match Hashtbl.find numeral_key_table (pattern_key c) with
+      | (_,_,None) -> raise No_match
+      | (sc,_,Some numpr) ->
+	  match numpr c with
+	    | None -> raise No_match
+	    | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let availability_of_numeral printer_scope scopes =
+  match 
+    let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+    find_without_delimiters f printer_scope scopes
+  with
+    | None -> None
+    | Some x -> Some x
+
+(* Miscellaneous *)
+
+let exists_notation_in_scope scope prec ntn r =
+  try
+    let sc = Stringmap.find scope !scope_map in
+    let (r',(prec',_)) = Stringmap.find ntn sc.notations in
+    r' = r & prec = prec'
+  with Not_found -> false
+
+let exists_notation_prec prec nt sc =
+  try fst (snd (Stringmap.find nt sc.notations)) = prec with Not_found -> false
+
+let exists_notation prec nt =
+  Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc)
+    !scope_map false 
+
 (* Exportation of scopes *)
 let cache_scope (_,sc) =
   check_scope sc;
@@ -238,19 +311,8 @@ let (inScope,outScope) =
 
 let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
 
-
 (* Special scopes associated to arguments of a global reference *)
 
-open Libnames
-
-module RefOrdered =
-  struct
-    type t = global_reference
-    let compare = Pervasives.compare
-  end
-
-module Refmap = Map.Make(RefOrdered)
-
 let arguments_scope = ref Refmap.empty
 
 let cache_arguments_scope (_,(r,scl)) =
@@ -276,18 +338,22 @@ let find_arguments_scope r =
 
 (* Printing *)
 
-let pr_delimiters = function
+let pr_delimiters_info = function
   | None -> str "No delimiters"
   | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r
 
-let pr_notation prraw ntn r =
-  str ntn ++ str " stands for " ++ prraw r
+let rec rawconstr_of_aconstr () x =
+  map_aconstr_with_binders_loc dummy_loc (fun id () -> (id,())) 
+    rawconstr_of_aconstr () x
+
+let pr_notation_info prraw ntn c =
+  str ntn ++ str " stands for " ++ prraw (rawconstr_of_aconstr () c)
 
 let pr_named_scope prraw scope sc =
   str "Scope " ++ str scope ++ fnl ()
-  ++ pr_delimiters sc.delimiters ++ fnl ()
+  ++ pr_delimiters_info sc.delimiters ++ fnl ()
   ++ Stringmap.fold
-       (fun ntn (r,_) strm -> pr_notation prraw ntn r ++ fnl () ++ strm)
+       (fun ntn (r,(_,df)) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
 let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
@@ -297,20 +363,44 @@ let pr_scopes prraw =
    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
    !scope_map (mt ())
 
+(**********************************************************************)
+(* Mapping notations to concrete syntax *)
+
+type unparsing_rule = unparsing list * precedence
+
+(* Concrete syntax for symbolic-extension table *)
+let printing_rules = 
+  ref (Stringmap.empty : unparsing_rule Stringmap.t)
+
+let declare_notation_printing_rule ntn unpl =
+  printing_rules := Stringmap.add ntn unpl !printing_rules
+
+let find_notation_printing_rule ntn =
+  try Stringmap.find ntn !printing_rules
+  with Not_found -> anomaly ("No printing rule found for "^ntn)
+
+(**********************************************************************)
 (* Synchronisation with reset *)
 
-let freeze () = (!scope_map, !scope_stack, !arguments_scope)
+let freeze () =
+ (!scope_map, !scope_stack, !arguments_scope,
+  !notations_key_table, !printing_rules)
 
-let unfreeze (scm,scs,asc) =
+let unfreeze (scm,scs,asc,fkm,pprules) =
   scope_map := scm;
   scope_stack := scs;
-  arguments_scope := asc
+  arguments_scope := asc;
+  notations_key_table := fkm;
+  printing_rules := pprules
 
-let init () = ()
+let init () =
 (*
   scope_map := Strinmap.empty;
   scope_stack := Stringmap.empty
+  arguments_scope := Refmap.empty
 *)
+  notations_key_table := Gmapl.empty;
+  printing_rules := Stringmap.empty
 
 let _ = 
   declare_summary "symbols"
@@ -318,14 +408,3 @@ let _ =
       unfreeze_function = unfreeze;
       init_function = init;
       survive_section = false }
-
-
-let printing_rules = 
-  ref (Stringmap.empty : (unparsing list * precedence) Stringmap.t)
-
-let declare_printing_rule ntn unpl =
-  printing_rules := Stringmap.add ntn unpl !printing_rules
-
-let find_notation_printing_rule ntn =
-  try Stringmap.find ntn !printing_rules
-  with Not_found -> anomaly ("No printing rule found for "^ntn)
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 3c082b2ce..466a2bb28 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -14,22 +14,17 @@ open Pp
 open Bignat
 open Names
 open Nametab
+open Libnames
 open Rawterm
 open Topconstr
 open Ppextend
-(*i*)
 
-(*s A numeral interpreter is the pair of an interpreter for _integer_
-   numbers in terms and an optional interpreter in pattern, if
-   negative numbers are not supported, the interpreter must fail with
-   an appropriate error message *)
+(*i*)
 
-type numeral_interpreter_name = string
-type numeral_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
+(**********************************************************************)
+(* Scopes *)
 
-(* A scope is a set of interpreters for symbols + optional
+(*s A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
 type level = precedence * precedence list
@@ -38,40 +33,92 @@ type scope
 type scopes = scope_name list
 
 val default_scope : scope_name
+val declare_scope : scope_name -> unit
+
+(* Open scope *)
+
 val current_scopes : unit -> scopes
 val open_scope : scope_name -> unit
-val declare_scope : scope_name -> unit
 
 (* Declare delimiters for printing *)
+
 val declare_delimiters : scope_name -> delimiters -> unit
+val find_delimiters : scope_name -> delimiters option
+
+(*s Declare and uses back and forth a numeral interpretation *)
+
+(* A numeral interpreter is the pair of an interpreter for _integer_
+   numbers in terms and an optional interpreter in pattern, if
+   negative numbers are not supported, the interpreter must fail with
+   an appropriate error message *)
+
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
 
-(* Declare, interpret, and look for a printer for numeral *)
-val declare_numeral_interpreter :
-  numeral_interpreter_name -> numeral_interpreter -> unit
+type required_module = string list 
+val declare_numeral_interpreter : scope_name -> required_module ->
+  num_interpreter -> num_uninterpreter -> unit
+
+(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
 val interp_numeral : loc -> bigint -> scopes -> rawconstr
 val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern
-val find_numeral_printer : string -> scopes ->
-  (delimiters option * scopes) option
 
-(* Declare, interpret, and look for a printer for symbolic notations *)
-val declare_notation : notation -> scope_name -> aconstr * level -> unit
+(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
+(* such numeral *)
+val uninterp_numeral : rawconstr -> scope_name * bigint
+val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
+
+val availability_of_numeral : scope_name -> scopes -> scope_name option option
+
+(*s Declare and interpret back and forth a notation *)
+
+type interpretation = identifier list * aconstr
+
+(* Binds a notation in a given scope to an interpretation *)
+type interp_rule = scope_name * notation * interpretation * int option
+val declare_notation : notation -> scope_name -> interpretation -> level ->
+  string -> bool -> unit
+
+(* Returns the interpretation bound to a notation *)
 val interp_notation : notation -> scopes -> aconstr
-val find_notation : scope_name -> notation -> scopes -> 
-  (delimiters option * scopes) option
-val exists_notation_in_scope : 
-  scope_name -> level -> notation -> aconstr -> bool
+
+(* Returns the possible notations for a given term *)
+val uninterp_notations : rawconstr -> interp_rule list
+
+(* Test if a notation is available in the scopes *)
+(* context [scopes] if available, the result is not None; the first *)
+(* argument is itself not None if a delimiters is needed; the second *)
+(* argument is a numeral printer if the *)
+val availability_of_notation : scope_name * notation -> scopes -> 
+  scope_name option option
+
+(*s** Miscellaneous *)
+
+(* Checks for already existing notations *)
+val exists_notation_in_scope : scope_name -> level -> notation -> aconstr->bool
 val exists_notation : level -> notation -> bool
 
-(* Declare and look for scopes associated to arguments of a global ref *)
-open Libnames
+(* Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope: global_reference -> scope_name option list -> unit
 val find_arguments_scope : global_reference -> scope_name option list
 
-(* Printing scopes *)
-val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds
-val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds
+(* Prints scopes (expect a pure aconstr printer *)
+val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
+
+(**********************************************************************)
+(*s Printing rules for notations *)
 
+(* Declare and look for the printing rule for symbolic notations *)
+type unparsing_rule = unparsing list * precedence
+val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
 
-val declare_printing_rule : notation -> unparsing list * precedence -> unit
-val find_notation_printing_rule : notation -> unparsing list * precedence
+(**********************************************************************)
+(* Rem: printing rules for numerals are trivial *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8d16602b5..8173d3fc4 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -18,8 +18,9 @@ open Rawterm
 open Term
 (*i*)
 
-
+(**********************************************************************)
 (* This is the subtype of rawconstr allowed in syntactic extensions *)
+
 type aconstr =
   | ARef of global_reference
   | AVar of identifier
@@ -29,7 +30,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option * aconstr list *
       (identifier list * cases_pattern list * aconstr) list
-  | AOldCase of case_style * aconstr option * aconstr * aconstr array
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
   | AMeta of int
@@ -53,7 +54,7 @@ let map_aconstr_with_binders_loc loc g f e = function
       let eqnl = List.map (fun (idl,pat,rhs) ->
         let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
       RCases (loc,option_app (f e) tyopt,List.map (f e) tml,eqnl)
-  | AOldCase (b,tyopt,tm,bv) ->
+  | AOrderedCase (b,tyopt,tm,bv) ->
       ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
   | ACast (c,t) -> RCast (loc,f e c,f e t)
   | ASort x -> RSort (loc,x)
@@ -114,12 +115,12 @@ let rec subst_aconstr subst raw =
         if ro' == ro && rl' == rl && branches' == branches then raw else
           ACases (ro',rl',branches')
 
-  | AOldCase (b,ro,r,ra) -> 
+  | AOrderedCase (b,ro,r,ra) -> 
       let ro' = option_smartmap (subst_aconstr subst) ro
       and r' = subst_aconstr subst r 
       and ra' = array_smartmap (subst_aconstr subst) ra in
 	if ro' == ro && r' == r && ra' == ra then raw else
-	  AOldCase (b,ro',r',ra')
+	  AOrderedCase (b,ro',r',ra')
 
   | AMeta _ | ASort _ -> raw
 
@@ -145,7 +146,7 @@ let rec aux = function
       let eqnl = List.map (fun (_,idl,pat,rhs) -> (idl,pat,aux rhs)) eqnl in
       ACases (option_app aux tyopt,List.map aux tml, eqnl)
   | ROrderedCase (_,b,tyopt,tm,bv) ->
-      AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -157,6 +158,75 @@ allowed in abbreviatable expressions"
 
 let aconstr_of_rawconstr = aux
 
+(* Pattern-matching rawconstr and aconstr *)
+
+exception No_match
+
+let rec alpha_var id1 id2 = function
+  | (i1,i2)::_ when i1=id1 -> i2 = id2
+  | (i1,i2)::_ when i2=id2 -> i1 = id1
+  | _::idl -> alpha_var id1 id2 idl
+  | [] -> id1 = id2
+
+let alpha_eq_val (x,y) = x = y
+
+let bind_env sigma var v =
+  try
+    let vvar = List.assoc var sigma in
+    if alpha_eq_val (v,vvar) then sigma
+    else raise No_match
+  with Not_found -> 
+    (var,v)::sigma
+
+let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
+  | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
+  | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
+  | RMeta (_,n1), AMeta n2 when n1=n2 -> sigma
+  | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+      List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
+  | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     let sigma = List.fold_left2 (match_ alp metas) sigma tml1 tml2 in
+     List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
+  | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
+  | RCast(_,c1,t1), ACast(c2,t2) ->
+      match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
+  | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
+  | RHole _, a -> sigma
+  | a, AHole _ -> sigma
+  | (RDynamic _ | RRec _ | REvar _), _ 
+  | _,_ -> raise No_match
+
+and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
+  | (na1,Name id2) when List.mem id2 metas ->
+      let sigma =
+	name_fold
+	  (fun id sigma -> bind_env sigma id2 (RVar (dummy_loc,id))) na1 sigma
+      in 
+      match_ alp metas sigma b1 b2
+  | (na1,na2) -> 
+      let alp =
+        name_fold
+	  (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in
+      match_ alp metas sigma b1 b2
+
+and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
+  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
+    match_ alp metas sigma rhs1 rhs2
+  else raise No_match
+
+let match_aconstr c (metas,pat) = match_ [] metas [] c pat
+
+(**********************************************************************)
 (*s Concrete syntax for terms *)
 
 type scope_name = string
@@ -200,6 +270,16 @@ and fixpoint_expr = identifier * int * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
+(***********************)
+(* For binders parsing *)
+
+type local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+(**********************************************************************)
+(* Functions on constr_expr *)
+
 let constr_loc = function
   | CRef (Ident (loc,_)) -> loc
   | CRef (Qualid (loc,_)) -> loc
@@ -230,9 +310,6 @@ let cases_pattern_loc = function
   | CPatNumeral (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
-let replace_vars_constr_expr l t =
-  if l = [] then t else failwith "replace_constr_expr: TODO"
-
 let occur_var_constr_ref id = function
   | Ident (loc,id') -> id = id'
   | Qualid _ -> false
@@ -307,12 +384,14 @@ let map_constr_expr_with_binders f g e = function
   | CCoFix (loc,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
 
-(* For binders parsing *)
-
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
+(* Used in constrintern *)
+let rec replace_vars_constr_expr l = function
+  | CRef (Ident (loc,id)) as x ->
+      (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
+  | c -> map_constr_expr_with_binders replace_vars_constr_expr 
+      (fun id l -> List.remove_assoc id l) l c
 
+(**********************************************************************)
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2c276ca99..85b05a4fa 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -31,7 +31,7 @@ type aconstr =
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option * aconstr list *
       (identifier list * cases_pattern list * aconstr) list
-  | AOldCase of case_style * aconstr option * aconstr * aconstr array
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ASort of rawsort
   | AHole of hole_kind
   | AMeta of int
@@ -45,6 +45,12 @@ val subst_aconstr : Names.substitution -> aconstr -> aconstr
 
 val aconstr_of_rawconstr : rawconstr -> aconstr
 
+(* [match_aconstr metas] match a rawconstr against an aconstr with
+   metavariables in [metas]; it raises [No_match] if the matching fails *)
+exception No_match
+val match_aconstr : 
+  rawconstr -> (identifier list * aconstr) -> (identifier * rawconstr) list
+
 (*s Concrete syntax for terms *)
 
 type scope_name = string
diff --git a/parsing/ast.ml b/parsing/ast.ml
index ae677979f..13989bcbb 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -345,6 +345,8 @@ let rec amatch alp sigma spat ast =
     | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
     | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
         amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
+    | (Pmeta_slam(pv,pb), Slam(loc, None, b)) ->
+        amatch alp (bind_env_ast sigma pv (Nvar(loc,id_of_string "_"))) pb b
     | (Pmeta_slam(pv,pb), Smetalam(loc, s, b)) ->
 	anomaly "amatch: match a pattern with an open ast"
     | (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op ->
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 33ca1214f..5b5777492 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -20,7 +20,7 @@ open Libnames
 (* State of the grammar extensions *)
 
 type all_grammar_command =
-  | Notation of (string * notation * prod_item list)
+  | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
   | Delimiters of (scope_name * prod_item list * prod_item list)
   | Grammar of grammar_command
   | TacticGrammar of
@@ -35,6 +35,35 @@ let subst_all_grammar_command subst = function
 
 let (grammar_state : all_grammar_command list ref) = ref []
 
+
+(**************************************************************************)
+let constr_level = function
+  | 8 -> "top"
+  | n -> string_of_int n
+
+let symbolic_level = function
+  | 9 -> "constr9", None
+  | 10 -> "lconstr", None
+  | 11 -> "pattern", None
+  | n -> "constr", Some n
+
+let numeric_levels = ref [8;1;0]
+
+exception Found
+
+let find_position n =
+  let after = ref 8 in
+  let rec add_level q = function
+    | p::l when p > n -> p :: add_level p l
+    | p::l when p = n -> raise Found
+    | l -> after := q; n::l
+  in
+  try
+    numeric_levels := add_level 8 !numeric_levels;
+    Gramext.After (constr_level !after)
+  with
+      Found -> Gramext.Level (constr_level n)
+
 (* Interpretation of the right hand side of grammar rules *)
 
 (* When reporting errors, we add the name of the grammar rule that failed *)
@@ -78,13 +107,15 @@ let make_act f pil =
 	Gramext.action (fun loc -> f loc env)
     | None :: tl -> (* parse a non-binding item *)
         Gramext.action (fun _ -> make env tl)
-    | Some (p, ETConstr) :: tl -> (* non-terminal *)
+    | Some (p, (ETConstr _| ETOther _)) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
     | Some (p, ETIdent) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:identifier) ->
-	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) in
+	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+    | Some (p, ETPattern) :: tl -> 
+	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
 
 let make_cases_pattern_act f pil =
@@ -93,12 +124,12 @@ let make_cases_pattern_act f pil =
 	Gramext.action (fun loc -> f loc env)
     | None :: tl -> (* parse a non-binding item *)
         Gramext.action (fun _ -> make env tl)
-    | Some (p, ETConstr) :: tl -> (* non-terminal *)
+    | Some (p, ETPattern) :: tl -> (* non-terminal *)
         Gramext.action (fun v -> make ((p,v) :: env) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
-    | Some (p, ETIdent) :: tl ->
-	error "ident entry not admitted in patterns cases syntax extensions" in
+    | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
+	error "ident and constr entry not admitted in patterns cases syntax extensions" in
   make [] (List.rev pil)
 
 (* Grammar extension command. Rules are assumed correct.
@@ -108,17 +139,16 @@ let make_cases_pattern_act f pil =
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let get_entry_type (u,n) =
-  if u = "constr" & n = "pattern" then Gram.Entry.obj Constr.pattern
-  else Gram.Entry.obj (object_of_typed_entry (get_entry (get_univ u) n))
-
 let rec build_prod_item univ = function
   | ProdList0 s -> Gramext.Slist0 (build_prod_item univ s)
   | ProdList1 s -> Gramext.Slist1 (build_prod_item univ s)
   | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ s)
-  | ProdPrimitive nt -> 
-      let eobj = get_entry_type nt in
-      Gramext.Snterm eobj
+  | ProdPrimitive typ ->
+      match entry_of_type false typ with
+	| (eobj,None) ->
+	    Gramext.Snterm (Gram.Entry.obj eobj)
+	| (eobj,Some lev) ->
+	    Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
 
 let symbol_of_prod_item univ = function
   | Term tok -> (Gramext.Stoken tok, None)
@@ -126,14 +156,6 @@ let symbol_of_prod_item univ = function
       let eobj = build_prod_item univ nt in
       (eobj, ovar)
 
-(*
-let make_rule univ etyp rule =
-  let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
-  let (symbs,ntl) = List.split pil in
-  let act = make_act (rule.gr_name,etyp) rule.gr_action ntl in
-  (symbs, act)
-*)
-
 let make_rule univ etyp rule =
   let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
   let (symbs,ntl) = List.split pil in
@@ -147,18 +169,19 @@ let make_rule univ etyp rule =
   let act = make_act f ntl in
   (symbs, act)
 
-
 (* Rules of a level are entered in reverse order, so that the first rules
    are applied before the last ones *)
-let extend_entry univ (te, etyp, ass, rls) =
+let extend_entry univ (te, etyp, pos, name, ass, rls) =
   let rules = List.rev (List.map (make_rule univ etyp) rls) in
-  grammar_extend (object_of_typed_entry te) None [(None, ass, rules)]
+  grammar_extend te pos [(name, ass, rules)]
 
 (* Defines new entries. If the entry already exists, check its type *)
-let define_entry univ {ge_name=n; ge_type=typ; gl_assoc=ass; gl_rules=rls} =
-  let typ = entry_type_of_constr_entry_type typ in
-  let e = force_entry_type univ n typ in
-  (e,typ,ass,rls)
+let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} =
+  let typ = explicitize_entry (fst univ) n in
+  let e,lev = entry_of_type true typ in
+  let pos = option_app find_position lev in
+  let name = option_app constr_level lev in
+  (e,typ,pos,name,ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
 let extend_grammar_rules gram =
@@ -186,29 +209,31 @@ let make_gen_act f pil =
         Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
   make [] (List.rev pil)
 
-let extend_constr entry make_act pt =
+let extend_constr entry pos (level,assoc) make_act pt =
   let univ = get_univ "constr" in
   let pil = List.map (symbol_of_prod_item univ) pt in
   let (symbs,ntl) = List.split pil in
   let act = make_act ntl in
-  grammar_extend entry None [(None, None, [symbs, act])]
+  grammar_extend entry pos [(level, assoc, [symbs, act])]
 
 let constr_entry name =
   object_of_typed_entry (get_entry (get_univ "constr") name)
 
-let extend_constr_notation (name,ntn,rule) =
+let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,env) in
-  extend_constr (constr_entry name) (make_act mkact) rule
-
-let extend_constr_grammar (name,c,rule) =
-  let mkact loc env = CGrammar (loc,c,env) in
-  extend_constr (constr_entry name) (make_act mkact) rule
+  let (e,level) = entry_of_type false (ETConstr ((n,Ppextend.E),Some n)) in
+  let pos = option_app find_position level in
+  extend_constr e pos (option_app constr_level level,assoc) 
+    (make_act mkact) rule
 
 let extend_constr_delimiters (sc,rule,pat_rule) =
   let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr (constr_entry "constr8") (make_act mkact) rule;
+  extend_constr (constr_entry "constr") (Some (Gramext.Level "top"))
+    (None,None)
+    (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.pattern (make_cases_pattern_act mkact) pat_rule
+  extend_constr Constr.pattern None (None,None)
+    (make_cases_pattern_act mkact) pat_rule
 
 (* These grammars are not a removable *)
 let make_rule univ f g (s,pt) =
@@ -246,7 +271,7 @@ let rec interp_entry_name u s =
     let e = get_entry (get_univ u) n in
     let o = object_of_typed_entry e in
     let t = type_of_typed_entry e in
-    t, Gramext.Snterm (Pcoq.Gram.Entry.obj o)
+    t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
 
 let qualified_nterm current_univ = function
   | NtQual (univ, en) -> (rename_command univ, rename_command en)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index ff3f6284b..d24264abc 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -24,15 +24,13 @@ val unfreeze : frozen_t -> unit
 val init : unit -> unit
 
 type all_grammar_command =
-  | Notation of (string * notation * prod_item list)
+  | Notation of (int * Gramext.g_assoc option * notation * prod_item list)
   | Delimiters of (scope_name * prod_item list * prod_item list)
   | Grammar of grammar_command
   | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list
 
 val extend_grammar : all_grammar_command -> unit
 
-val extend_constr_grammar : string * aconstr * prod_item list -> unit
-
 (* Add grammar rules for tactics *)
 type grammar_tactic_production =
   | TacTerm of string
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 76f4b3f19..859b5548a 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -186,7 +186,8 @@ let pr_parenthesis inherited se strm =
     
 let print_delimiters inh se strm = function
   | None -> pr_parenthesis inh se strm
-  | Some (left,right) ->
+  | Some sc ->
+      let (left,right) = out_some (find_delimiters sc) in
       assert (left <> "" && right <> "");
       let lspace =
 	if is_letter (left.[String.length left -1]) then str " " else mt () in
@@ -227,21 +228,21 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
 	  (* Test for a primitive printer; may raise Not_found *)
 	  let sc,pr = lookup_primitive_printer c in
 	  (* Look if scope [sc] associated to this printer is OK *)
-	  (match Symbols.find_numeral_printer sc scopes with
+	  (match Symbols.availability_of_numeral sc scopes with
 	    | None -> otherwise ()
-	    | Some (dlm,scopes) ->
+	    | Some scopt ->
 	        (* We can use this printer *)
 	        let node = Ast.pat_sub dummy_loc env e in
 	        match pr node with
-		  | Some strm -> print_delimiters inherited se strm dlm
+		  | Some strm -> print_delimiters inherited se strm scopt
 		  | None -> otherwise ())
     | [UNP_SYMBOLIC (sc,pat,sub)] ->
-	(match Symbols.find_notation sc pat scopes with
+	(match Symbols.availability_of_notation (sc,pat) scopes with
 	  | None -> otherwise ()
-	  | Some (dlm,scopes) ->
+	  | Some scopt ->
 	      print_delimiters inherited se
-		(print_syntax_entry rec_pr scopes env 
-		  {se with syn_hunks = [sub]}) dlm)
+		(print_syntax_entry rec_pr (option_cons scopt scopes) env 
+		  {se with syn_hunks = [sub]}) scopt)
     | _ ->
 	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
   )
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 0e1f72536..2e4eea4b0 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -19,13 +19,17 @@ open Topconstr
 open Genarg
 
 type entry_type = argument_type
-type constr_entry_type = ETConstr | ETIdent | ETReference
+type constr_entry_type =
+  | ETIdent | ETReference
+  | ETConstr of (int * parenRelation) * int option
+  | ETPattern
+  | ETOther of string * string
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of (string * string)
+  | ProdPrimitive of constr_entry_type
 
 type prod_item =
   | Term of Token.pattern
@@ -38,7 +42,6 @@ type grammar_rule = {
 
 type grammar_entry = { 
   ge_name : string;
-  ge_type : constr_entry_type;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -56,18 +59,20 @@ type entry_context = (identifier * constr_entry_type) list
 let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z"))
 let set_ast_to_rawconstr f = ast_to_rawconstr := f
 
-let act_of_ast vars = function
-  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
-  | SimpleAction (loc,CasesPatternNode a) -> failwith "TODO:act_of_ast: cases_pattern"
+let act_of_ast env = function
+  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr env a
+  | SimpleAction (loc,CasesPatternNode a) -> 
+      failwith "TODO:act_of_ast: cases_pattern"
   | CaseAction _ -> failwith "case/let not supported"
 
 let to_act_check_vars = act_of_ast
 
 type syntax_modifier =
-  | SetItemLevel of string * int
+  | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * constr_entry_type
+  | SetOnlyParsing
 
 type nonterm =
   | NtShort of string
@@ -76,8 +81,7 @@ type grammar_production =
   | VTerm of string
   | VNonTerm of loc * nonterm * Names.identifier option
 type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = 
-  string * constr_entry_type * grammar_associativity * raw_grammar_rule list
+type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 let subst_grammar_rule subst gr =
   { gr with gr_action = subst_aconstr subst gr.gr_action }
@@ -141,55 +145,85 @@ let rename_command nt =
   else if nt = "lassoc_command4" then warn nt "lassoc_constr4"
   else nt
 
-let qualified_nterm current_univ = function
-  | NtQual (univ, en) -> (rename_command univ, rename_command en)
-  | NtShort en -> (current_univ, rename_command en)
-
-let entry_type_of_constr_entry_type = function
-  | ETConstr -> ConstrArgType
-  | ETIdent -> IdentArgType
-  | ETReference -> RefArgType
-
-let constr_entry_of_entry = function
-  | ConstrArgType -> ETConstr
-  | IdentArgType -> ETIdent
-  | RefArgType -> ETReference
-  | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
-
-let nterm loc (get_entry_type,univ) nont =
-  let nt = qualified_nterm univ nont in
-  try (nt,constr_entry_of_entry (get_entry_type nt))
-  with Not_found -> 
-    let (s,n) = nt in
-    user_err_loc(loc,"Externd.nterm",str("unknown grammar entry: "^s^":"^n))
+(* This translates constr0, constr1, ... level into camlp4 levels of constr *)
+
+let explicitize_entry univ nt =
+  if univ = "prim" & nt = "var" then ETIdent else
+  if univ <> "constr" then ETOther (univ,nt) else
+  match nt with
+  | "constr0" -> ETConstr ((0,E),Some 0)
+  | "constr1" -> ETConstr ((1,E),Some 1)
+  | "constr2" -> ETConstr ((2,E),Some 2)
+  | "constr3" -> ETConstr ((3,E),Some 3)
+  | "lassoc_constr4" -> ETConstr ((4,E),Some 4)
+  | "constr5" -> ETConstr ((5,E),Some 5)
+  | "constr6" -> ETConstr ((6,E),Some 6)
+  | "constr7" -> ETConstr ((7,E),Some 7)
+  | "constr8" | "constr" -> ETConstr ((8,E),Some 8)
+  | "constr9" -> ETConstr ((9,E),Some 9)
+  | "constr10" | "lconstr" -> ETConstr ((10,E),Some 10)
+  | "ident" -> ETIdent
+  | "global" -> ETReference
+  | _ -> ETOther (univ,nt)
+
+(* This determines if a reference to constr_n is a reference to the level
+   below wrt associativity (to be translated in camlp4 into "constr" without 
+   level) or to another level (to be translated into "constr LEVEL n") *)
+
+let clever_explicitize_entry univ name from assoc pos =
+  match explicitize_entry univ name, explicitize_entry "" from, pos with
+    | ETConstr ((n,_ as s),_),ETConstr ((lev,_),_),Some start
+	when n = lev - 1 & assoc <> Some Gramext.LeftA & start
+	  or n = lev & assoc = Some Gramext.LeftA & start
+	  or n = lev & assoc = Some Gramext.RightA & not start
+	  or n = lev - 1 & assoc <> Some Gramext.RightA & not start
+	-> ETConstr (s, None)
+    | x,_,_ -> x
+
+let qualified_nterm current_univ from ass pos = function
+  | NtQual (univ, en) ->
+      let univ = rename_command univ in
+      clever_explicitize_entry univ (rename_command en) from ass pos
+  | NtShort en ->
+      clever_explicitize_entry current_univ (rename_command en) from ass pos
+
+let check_entry check_entry_type = function
+  | ETOther (u,n) -> check_entry_type (u,n)
+  | _ -> ()
+
+let nterm loc (((check_entry_type,univ),lev,ass),pos) nont =
+  let typ = qualified_nterm univ lev ass pos nont in
+  check_entry check_entry_type typ;
+  typ
 
 let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
-     let (nont, etyp) = nterm loc univ nt in
-      ((p, etyp) :: env, NonTerm (ProdPrimitive nont, Some (p,etyp)))
+     let typ = nterm loc univ nt in
+      ((p, typ) :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
-      let (nont, etyp) = nterm loc univ nt in 
-      env, NonTerm (ProdPrimitive nont, None)
+      let typ = nterm loc univ nt in 
+      env, NonTerm (ProdPrimitive typ, None)
 
-let rec prod_item_list univ penv pil =
+let rec prod_item_list univ penv pil start =
   match pil with
     | [] -> [], penv
     | pi :: pitl ->
-	let (env, pic) = prod_item univ penv pi in
-	let (pictl, act_env) = prod_item_list univ env pitl in
+	let pos = if pitl=[] then Some false else start in
+	let (env, pic) = prod_item (univ,pos) penv pi in
+	let (pictl, act_env) = prod_item_list univ env pitl None in
         (pic :: pictl, act_env)
 
-let gram_rule univ etyp (name,pil,act) =
-  let (pilc, act_env) = prod_item_list univ [] pil in
+let gram_rule univ (name,pil,act) =
+  let (pilc, act_env) = prod_item_list univ [] pil (Some true) in
   let a = to_act_check_vars act_env act in
   { gr_name = name; gr_production = pilc; gr_action = a }
 
-let gram_entry univ (nt, etyp, ass, rl) =
-  { ge_name = rename_command nt;
-    ge_type = etyp;
+let gram_entry univ (nt, ass, rl) =
+  let name = rename_command nt in
+  { ge_name = name;
     gl_assoc = ass;
-    gl_rules = List.map (gram_rule univ etyp) rl }
+    gl_rules = List.map (gram_rule (univ,name,ass)) rl }
 
 let interp_grammar_command univ ge entryl =
   let univ = rename_command univ in
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 13e3ee067..771434ea3 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -20,15 +20,17 @@ open Genarg
 (*i*)
 
 type entry_type = argument_type
-type constr_entry_type = ETConstr | ETIdent | ETReference
-
-val entry_type_of_constr_entry_type : constr_entry_type -> entry_type
+type constr_entry_type =
+  | ETIdent | ETReference
+  | ETConstr of (int * parenRelation) * int option
+  | ETPattern
+  | ETOther of string * string
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of (string * string)
+  | ProdPrimitive of constr_entry_type
 
 type prod_item =
   | Term of Token.pattern
@@ -41,7 +43,6 @@ type grammar_rule = {
 
 type grammar_entry = { 
   ge_name : string;
-  ge_type : constr_entry_type;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -57,10 +58,11 @@ val to_act_check_vars : entry_context -> grammar_action -> aconstr
 val set_ast_to_rawconstr : (entry_context -> constr_expr -> aconstr) -> unit
 
 type syntax_modifier =
-  | SetItemLevel of string * int
+  | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * constr_entry_type
+  | SetOnlyParsing
 
 type nonterm =
   | NtShort of string
@@ -69,13 +71,14 @@ type grammar_production =
   | VTerm of string
   | VNonTerm of loc * nonterm * Names.identifier option
 type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = 
-  string * constr_entry_type * grammar_associativity * raw_grammar_rule list
+type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 val terminal : string -> string * string
 
 val rename_command : string -> string
 
+val explicitize_entry : string -> string -> constr_entry_type
+
 val subst_grammar_command : 
   Names.substitution -> grammar_command -> grammar_command
 
@@ -90,10 +93,6 @@ type 'pat unparsing_hunk =
   | UNP_TAB
   | UNP_FNL
   | UNP_SYMBOLIC of string * string * 'pat unparsing_hunk
-(*
-  | UNP_INFIX of Libnames.extended_global_reference * string * string *
-      (parenRelation * parenRelation)
-*)
 
 (*val subst_unparsing_hunk : 
   Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> 
@@ -129,7 +128,7 @@ type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
 type raw_syntax_entry = precedence * syntax_rule list
 
 val interp_grammar_command :
-  string -> (string * string -> Genarg.argument_type) -> 
+  string -> (string * string -> unit) -> 
       raw_grammar_entry list -> grammar_command
 
 val interp_syntax_entry :
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 77f587894..55a350447 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -153,7 +153,8 @@ GEXTEND Gram
 	  VernacRemoveOption (PrimaryTable table, v) ] ]
   ;
   printable:
-    [ [ IDENT "All" -> PrintFullContext
+    [ [ IDENT "Term"; qid = global -> PrintName qid
+      | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
       | "Grammar"; uni = IDENT; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
@@ -173,7 +174,8 @@ GEXTEND Gram
       | IDENT "Hint" -> PrintHintGoal
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
-      | IDENT "HintDb"; s = IDENT  -> PrintHintDbName s ] ]
+      | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue n
@@ -217,14 +219,14 @@ GEXTEND Gram
      | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
-     | "Syntax"; IDENT "Extension"; s = STRING; 
+     | "Uninterpreted"; IDENT "Notation"; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (s,l)
 
      | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
 
-     | IDENT "Delimiters"; left = STRING; sc = IDENT; right = STRING ->
-	 VernacDelimiters (sc,(left,right))
+     | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
+	 VernacDelimiters (sc,("`"^key^":","`"))
 
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
@@ -233,23 +235,27 @@ GEXTEND Gram
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc)
      | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
-     | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr;
+     | IDENT "Notation"; s = IDENT; ":="; c = constr ->
+	 VernacNotation ("'"^s^"'",c,[],None)
+     | IDENT "Notation"; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-	   let a = match a with None -> Gramext.LeftA | Some a -> a in
-	   VernacNotation (s,c,(SetAssoc a)::(SetLevel n)::modl,sc)
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (s,c,modl,sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> SetItemLevel (x,n)
+    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
+        SetItemLevel ([x],n)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level";
+        n = natural -> SetItemLevel (x::l,n)
       | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
-      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ]
+      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference ] ]
@@ -259,9 +265,9 @@ GEXTEND Gram
   ;
   (* Syntax entries for Grammar. Only grammar_entry is exported *)
   grammar_entry:
-    [[ nont = IDENT; etyp = set_entry_type; ":=";
+    [[ nont = IDENT; set_entry_type; ":=";
        ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
-	 (nont,etyp,ep,rl) ]]
+	 (nont,ep,rl) ]]
   ;
   entry_prec:
     [[ IDENT "LEFTA" -> Some Gramext.LeftA
@@ -366,13 +372,8 @@ GEXTEND Gram
      | [ ":"; IDENT "ast" -> () | -> () ] -> Ast.ETast ]]
   ;
   set_entry_type:
-    [[ ":"; et = entry_type -> set_default_action_parser et;
-       let a = match et with
-	 | ConstrParser -> ETConstr
-	 | CasesPatternParser ->
-	     failwith "entry_type_of_parser: cases_pattern, TODO" in
-       a
-     | -> ETConstr ]]
+    [[ ":"; et = entry_type -> set_default_action_parser et
+     | -> () ]]
   ;
   entry_type:
     [[ IDENT "ast"; IDENT "list" -> Util.error "type ast list no longer supported"
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 1b8be4f4f..a7b27de23 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -20,7 +20,7 @@ let pair loc =
   Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair")
 
 GEXTEND Gram
-  GLOBAL: constr1 pattern;
+  GLOBAL: constr pattern;
 
   pattern:
     [ [ r = Prim.reference -> CPatAtom (loc,Some r)
@@ -52,8 +52,7 @@ GEXTEND Gram
   ne_eqn_list:
     [ [ leqn = LIST1 equation SEP "|" -> leqn ] ]
   ;
-
-  constr1:
+  constr: LEVEL "1"
     [ [ "<"; p = lconstr; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
 	  CCases (loc, Some p, lc, eqs)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8644cb724..6476cec51 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -52,12 +52,23 @@ let test_int_rparen =
             end
         | _ -> raise Stream.Failure)
 
+(* Hack to parse "n" at level 0 without conflicting with "n!" at level 91 *)
+(* admissible notation "(n)" *)
+let test_int_bang =
+  Gram.Entry.of_parser "test_int_bang"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("INT", n)] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("", "!")] -> ()
+              | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
+
 
 GEXTEND Gram
-  GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
-          constr6 constr7 constr8 constr9 constr10 lconstr constr
-          ne_name_comma_list ne_constr_list sort
-          global constr_pattern Constr.ident;
+  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident
+          (*ne_name_comma_list*);
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -70,12 +81,6 @@ GEXTEND Gram
       (* This is used in quotations *)
       | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
   ;
-  constr:
-    [ [ c = constr8 -> c ] ]
-  ;
-  lconstr:
-    [ [ c = constr10 -> c ] ]
-  ;
   constr_pattern:
     [ [ c = constr -> c ] ]
   ;
@@ -87,10 +92,47 @@ GEXTEND Gram
       | "Prop" -> RProp Null
       | "Type" -> RType None ] ]
   ;
-  constr0:
-    [ [ "?" -> CHole loc
+  constr:
+    [ "top" RIGHTA
+      [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
+    | "1"
+      [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, MatchStyle, Some p, c, cl)
+      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
+        cl = LIST0 constr; "end" ->
+	  COrderedCase (loc, RegularStyle, Some p, c, cl)
+      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
+          COrderedCase (loc, RegularStyle, None, c, cl)
+      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
+          COrderedCase (loc, MatchStyle, None, c, cl)
+      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
+        c = constr; "in"; c1 = constr LEVEL "top"->
+          (* TODO: right loc *)
+	  COrderedCase
+            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
+      | IDENT "let"; na = name; "="; c = opt_casted_constr; 
+	"in"; c1 = constr LEVEL "top" ->
+          CLetIn (loc, na, c, c1)
+      | IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr;
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+      | "<"; p = lconstr; ">";
+        IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; 
+        "in"; c1 = constr LEVEL "top" ->
+          (* TODO: right loc *)
+	  COrderedCase (loc, LetStyle, Some p, c,
+            [CLambdaN (loc, [b, CHole loc], c1)])
+      | "<"; p = lconstr; ">";
+        IDENT "if"; c1 = constr;
+        IDENT "then"; c2 = constr; 
+        IDENT "else"; c3 = constr LEVEL "top" ->
+	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
+    | "0"
+      [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CMeta (loc, n)
-      | bll = binders; c = constr -> abstract_constr loc c bll
+      | bll = binders; c = constr LEVEL "top" -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
       | "("; test_int_rparen; n = INT; ")" ->
 	  let n = CNumeral (loc,Bignat.POS (Bignat.of_string n)) in
@@ -99,7 +141,7 @@ GEXTEND Gram
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
 (* TODO: Syntaxe (_:t...)t et (_,x...)t *)
-      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr; 
+      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
         (bl,body) = product_tail ->
           let id1 = coerce_to_name lc1 in
           let id2 = coerce_to_name lc2 in
@@ -124,70 +166,11 @@ GEXTEND Gram
       | v = global -> CRef v
       | n = INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
       | "-"; n = INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n))
-      | "!"; f = global -> CAppExpl (loc,f,[])
-    ] ]
-  ;
-  constr1:
-    [ [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, MatchStyle, Some p, c, cl)
-      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
-        cl = LIST0 constr; "end" ->
-	  COrderedCase (loc, RegularStyle, Some p, c, cl)
-      | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
-          COrderedCase (loc, RegularStyle, None, c, cl)
-      | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
-          COrderedCase (loc, MatchStyle, None, c, cl)
-      | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr->
-          (* TODO: right loc *)
-	  COrderedCase
-            (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
-      | IDENT "let"; na = name; "="; c = opt_casted_constr; "in"; c1 = constr
-          -> CLetIn (loc, na, c, c1)
-      | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
-        IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
-      | "<"; p = lconstr; ">";
-        IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr ->
-          (* TODO: right loc *)
-	  COrderedCase (loc, LetStyle, Some p, c,
-            [CLambdaN (loc, [b, CHole loc], c1)])
-      | "<"; p = lconstr; ">";
-        IDENT "if"; c1 = constr; IDENT "then";
-        c2 = constr; IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3])
-      | c = constr0 -> c ] ]
-  ;
-  constr2: (* ~ will be here *)
-    [ [ c = constr1 -> c ] ]
+      | "!"; f = global -> CAppExpl (loc,f,[]) ] ]
   ;
-  constr3:
-    [ [ c1 = constr2 -> c1 ] ]
-  ;
-  lassoc_constr4:
-    [ [ c1 = constr3 -> c1 ] ]
-  ;
-  constr5:
-    [ [ c1 = lassoc_constr4 -> c1 ] ]
-  ;
-  constr6:  (* /\ will be here *)
-    [ [ c1 = constr5 -> c1 ] ]
-  ;
-  constr7:  (* \/ will be here *)
-    [ RIGHTA [ c1 = constr6 -> c1 ] ]
-  ;
-  constr8:  (* <-> will be here *)
-    [ [ c1 = constr7 -> c1
-      | c1 = constr7; "->"; c2 = constr8 -> CArrow (loc, c1, c2) ] ]
-  ;
-  constr9:
-    [ [ c1 = constr8 -> c1
-      | c1 = constr8; "::"; c2 = constr8 -> CCast (loc, c1, c2) ] ]
-  ;
-  constr10:
-    [ [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
+  lconstr:
+    [ "10"
+      [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
@@ -195,11 +178,19 @@ GEXTEND Gram
       | f = constr9; args = LIST1 constr91 -> CApp (loc, f, args)
       | f = constr9 -> f ] ]
   ;
+  constr91:
+    [ [ test_int_bang; n = INT; "!"; c = constr9 ->
+        (c, Some (int_of_string n))
+      | c = constr9 -> (c, None) ] ]
+  ;
+  constr9:
+    [ [ c1 = constr -> c1
+      | c1 = constr; "::"; c2 = constr -> CCast (loc, c1, c2) ] ]
+  ;
   ne_name_comma_list:
     [ [ nal = LIST1 name SEP "," -> nal ] ]
   ;
   name_comma_list_tail:
-
     [ [ ","; idl = ne_name_comma_list -> idl
       | -> [] ] ]
   ;
@@ -241,12 +232,6 @@ GEXTEND Gram
     [ [ ":"; c = constr -> c 
       | -> CHole loc ] ]
   ;
-  constr91:
-    [ [ n = natural; "!"; c = constr9 -> (c, Some n)
-      | n = natural ->
-          (CNumeral (loc, Bignat.POS (Bignat.of_string (string_of_int n))), None)
-      | c = constr9 -> (c, None) ] ]
-  ;
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 52100764d..951e75815 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -108,7 +108,7 @@ GEXTEND Gram
       | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
       | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
       | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c)
-      | IDENT "Extern"; n = natural; c = Constr.constr8 ; tac = tactic ->
+      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
 	  fun name -> HintsExtern (name,n,c,tac) ] ]
   ;
   hints:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 36619758a..7a8f82478 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -403,9 +403,19 @@ GEXTEND Gram
 	  Pp.warning "Class is obsolete"; VernacNop
 
 (* Implicit *)
+(*
       | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   VernacSyntacticDefinition (id,c,n)
+*)
+      | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr;
+         n = OPT [ "|"; n = natural -> n ] ->
+	   let c = match n with
+	     | Some n ->
+		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
+		 CApp (loc,c,l)
+	     | None -> c in
+	   VernacNotation ("'"^id^"'",c,[],None)
 
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6472dbaf5..fa0c3809e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -69,6 +69,7 @@ type typed_entry = entry_type * grammar_object G.Entry.e
 let in_typed_entry t e = (t,Gramobj.weaken_entry e)
 let type_of_typed_entry (t,e) = t
 let object_of_typed_entry (t,e) = e
+let weaken_entry x = Gramobj.weaken_entry x
 
 module type Gramtypes =
 sig
@@ -169,21 +170,6 @@ let map_entry f en =
 let parse_string f x =
   let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
 
-(*
-let entry_type ast =
-  match ast with
-    | Coqast.Id (_, "LIST") -> ETastl
-    | Coqast.Id (_, "AST") -> ETast
-    | _ -> invalid_arg "Ast.entry_type"
-*)
-
-(*
-let entry_type ast =
-  match ast with
-    | AstListType -> ETastl
-    | _ -> ETast
-*)
-
 type gram_universe = (string, typed_entry) Hashtbl.t
 
 let trace = ref false
@@ -353,27 +339,12 @@ module Constr =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     let constr = gec_constr "constr"
-    let constr0 = gec_constr "constr0"
-    let constr1 = gec_constr "constr1"
-    let constr2 = gec_constr "constr2"
-    let constr3 = gec_constr "constr3"
-    let lassoc_constr4 = gec_constr "lassoc_constr4"
-    let constr5 = gec_constr "constr5"
-    let constr6 = gec_constr "constr6"
-    let constr7 = gec_constr "constr7"
-    let constr8 = gec_constr "constr8"
     let constr9 = gec_constr "constr9"
-    let constr91 = gec_constr "constr91"
-    let constr10 = gec_constr "constr10"
     let constr_eoi = eoi_entry constr
     let lconstr = gec_constr "lconstr"
-    let sort = make_gen_entry uconstr rawwit_sort "sort"
-
     let ident = make_gen_entry uconstr rawwit_ident "ident"
     let global = make_gen_entry uconstr rawwit_ref "global"
-
-    let ne_name_comma_list = Gram.Entry.create "constr:ne_name_comma_list"
-    let ne_constr_list = gec_constr_list "ne_constr_list"
+    let sort = make_gen_entry uconstr rawwit_sort "sort"
     let pattern = Gram.Entry.create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
   end
@@ -520,3 +491,17 @@ let set_default_action_parser = function
 let default_action_parser =
   Gram.Entry.of_parser "default_action_parser" 
     (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
+
+let entry_of_type allow_create = function
+  | ETConstr (_,Some 10) -> weaken_entry Constr.lconstr, None
+  | ETConstr (_,Some 9) -> weaken_entry Constr.constr9, None
+  | ETConstr (_,lev) -> weaken_entry Constr.constr, lev
+  | ETIdent -> weaken_entry Constr.ident, None
+  | ETReference -> weaken_entry Constr.global, None
+  | ETOther (u,n) ->
+      let u = get_univ u in
+      let e =
+        try get_entry u n
+        with e when allow_create -> create_entry u n ConstrArgType in
+      object_of_typed_entry e, None
+  | ETPattern -> weaken_entry Constr.pattern, None
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a0f5a55c0..d46a245ce 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -30,6 +30,10 @@ type typed_entry
 
 val type_of_typed_entry : typed_entry -> Extend.entry_type
 val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
+val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
+
+val entry_of_type :
+  bool -> constr_entry_type -> grammar_object Gram.Entry.e * int option
 
 val grammar_extend :
   'a Gram.Entry.e -> Gramext.position option ->
@@ -56,6 +60,7 @@ val get_univ : string -> string * gram_universe
 val get_entry : string * gram_universe -> string -> typed_entry
 
 val entry_type : string * gram_universe -> string -> entry_type option
+
 val get_entry_type : string * string -> entry_type
 val create_entry_if_new :
   string * gram_universe -> string -> entry_type -> unit
@@ -118,30 +123,14 @@ module Prim :
 module Constr :
   sig
     val constr : constr_expr Gram.Entry.e
-    val constr0 : constr_expr Gram.Entry.e
-    val constr1 : constr_expr Gram.Entry.e
-    val constr2 : constr_expr Gram.Entry.e
-    val constr3 : constr_expr Gram.Entry.e
-    val lassoc_constr4 : constr_expr Gram.Entry.e
-    val constr5 : constr_expr Gram.Entry.e
-    val constr6 : constr_expr Gram.Entry.e
-    val constr7 : constr_expr Gram.Entry.e
-    val constr8 : constr_expr Gram.Entry.e
     val constr9 : constr_expr Gram.Entry.e
-    val constr91 : constr_expr Gram.Entry.e
-    val constr10 : constr_expr Gram.Entry.e
     val constr_eoi : constr_expr Gram.Entry.e
     val lconstr : constr_expr Gram.Entry.e
     val ident : identifier Gram.Entry.e
     val global : reference Gram.Entry.e
-    val ne_name_comma_list : name located list Gram.Entry.e
-    val ne_constr_list : constr_expr list Gram.Entry.e
     val sort : rawsort Gram.Entry.e
     val pattern : cases_pattern_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
-(*
-    val ne_binders_list : local_binder list Gram.Entry.e
-*)
   end
 
 module Module : 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index baac4a06d..e49f531f1 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -73,7 +73,12 @@ let wrap_exception = function
 
 let latom = 0
 let lannot = 1
-let lprod = 8
+let lprod = 1
+let llambda = 1
+let lif = 1
+let lletin = 1
+let lcases = 1
+let larrow = 8
 let lcast = 9
 let lapp = 10
 let ltop = (8,E)
@@ -98,7 +103,17 @@ let pr_notation pr s env =
   let unpl, level = find_notation_printing_rule s in
   prlist (print_hunk pr env) unpl, level
 
-let pr_delimiters x = failwith "pr_delimiters: TODO"
+let pr_delimiters sc strm =
+  match find_delimiters sc with
+  | None -> anomaly "Delimiters without concrete syntax"
+  | Some (left,right) ->
+  assert (left <> "" && right <> "");
+  let lspace =
+    if is_letter (left.[String.length left -1]) then str " " else mt () in
+  let rspace =
+    let c = right.[0] in
+    if is_letter c or is_digit c or c = '\'' then str " " else mt () in
+  str left ++ lspace ++ strm ++ rspace ++ str right
 
 open Rawterm
 
@@ -118,7 +133,7 @@ let pr_explicitation = function
   | Some n -> int n ++ str "!"
 
 let pr_expl_args pr (a,expl) =
-  pr_explicitation expl ++ pr (latom,E) a
+  pr_explicitation expl ++ pr (lapp,L) a
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
@@ -197,8 +212,8 @@ let pr_fix pr = pr_recursive "Fix" (pr_fixdecl pr)
 let pr_cofix pr = pr_recursive "Fix" (pr_cofixdecl pr)
 
 let rec pr_arrow pr = function
-  | CArrow (_,a,b) -> pr (lprod,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
-  | a -> pr (lprod,E) a
+  | CArrow (_,a,b) -> pr (larrow,L) a ++ cut () ++ str "->" ++ pr_arrow pr b
+  | a -> pr (larrow,E) a
 
 let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">"
 
@@ -209,25 +224,26 @@ let rec pr inherited a =
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) -> pr_fix pr (snd id) fix, latom
   | CCoFix (_,id,cofix) -> pr_cofix pr (snd id) cofix, latom
-  | CArrow _ -> hv 0 (pr_arrow pr a), lprod
+  | CArrow _ -> hv 0 (pr_arrow pr a), larrow
   | CProdN (_,bl,a) ->
       hov 0 (
 	str "(" ++ pr_binders pr bl ++ str ")" ++ brk(0,1) ++ pr ltop a), lprod
   | CLambdaN (_,bl,a) ->
       hov 0 (
-	str "[" ++ pr_binders pr bl ++ str "]" ++ brk(0,1) ++ pr ltop a), lprod
+	str "[" ++ pr_binders pr bl ++ str "]" ++ brk(0,1) ++ pr ltop a),
+      llambda
   | CLetIn (_,x,a,b) ->
-      hov 0 (pr_let_binder pr (snd x) a ++ cut () ++ pr ltop b), lprod
+      hov 0 (pr_let_binder pr (snd x) a ++ cut () ++ pr ltop b), lletin
   | CAppExpl (_,f,l) ->
       hov 0 (
-	str "!" ++ pr_reference f ++ 
-	prlist (fun a -> brk (1,1) ++ pr (latom,E) a) l), lapp
+	str "!" ++ pr_reference f ++
+	prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l), lapp
   | CApp (_,a,l) ->
       hov 0 (
 	pr (latom,E) a ++ 
 	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
   | CCases (_,po,c,eqns) ->
-      pr_cases po c eqns, lannot
+      pr_cases po c eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
@@ -236,7 +252,7 @@ let rec pr inherited a =
 	hv 0 (
 	  str "if" ++ pr ltop c ++ spc () ++
 	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
-	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lapp
+	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
   | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,_ as bd],b)]) ->
       hov 0 (
 	pr_opt (pr_annotation pr) po ++
@@ -245,7 +261,7 @@ let rec pr inherited a =
 	  hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++
 	  str "=" ++ brk (1,1) ++
 	  pr ltop c ++ spc () ++
-	  str "in " ++ pr ltop b)), lapp
+	  str "in " ++ pr ltop b)), lletin
   | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
       hov 0 (
 	hov 0 (
@@ -256,7 +272,7 @@ let rec pr inherited a =
 	    str (if style=RegularStyle then "of" else "with") ++
 	  brk (1,3) ++
 	  hov 0 (prlist (fun b -> pr ltop b ++ fnl ()) bl)) ++
-	str "end")), lannot
+	str "end")), lcases
   | COrderedCase (_,_,_,_,_) -> 
       anomaly "malformed if or destructuring let"
   | CHole _ -> str "?", latom
@@ -267,8 +283,7 @@ let rec pr inherited a =
   | CNotation (_,s,env) -> pr_notation pr s env
   | CGrammar _ -> failwith "CGrammar: TODO"
   | CNumeral (_,p) -> Bignat.pr_bigint p, latom
-  | CDelimiters (_,sc,a) -> failwith "pr_delim: TODO"
-(*      pr_delimiters (find_delimiters) (pr_constr_expr a)*)
+  | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
   | CDynamic _ -> str "<dynamic>", latom
   in
   if prec_less prec inherited then strm
@@ -352,8 +367,10 @@ let gentermpr gt =
 (* [at_top] means ids of env must be avoided in bound variables *)
 let gentermpr_core at_top env t =
   gentermpr (Termast.ast_of_constr at_top env t)
+
 (*
 let gentermpr_core at_top env t =
   pr_constr (Constrextern.extern_constr at_top env t)
 *)
 
+
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 6305cd650..7777ac540 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -76,7 +76,10 @@ let pr_ref_label = function (* On triche sur le contexte *)
   | VarNode id -> pr_id id
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
+(*
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
+*)
+let pr_rawterm t = pr_constr (Constrextern.extern_rawconstr t)
 let pr_pattern_env tenv env t = gentermpr (Termast.ast_of_pattern tenv env t)
 let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
 
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 6cc0d71c4..77ecf144d 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -199,7 +199,7 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 Module R_scope.
 
-Delimiters "'R:" R_scope "'".
+Delimits Scope R_scope with R.
 Infix NONA 5 "<=" Rle : R_scope.
 Infix NONA 5 "<"  Rlt : R_scope.
 Infix NONA 5 ">=" Rge : R_scope.
@@ -209,12 +209,17 @@ Infix 4 "-" Rminus : R_scope.
 Infix 3 "*" Rmult : R_scope.
 Infix LEFTA 3 "/" Rdiv : R_scope.
 Distfix 0 "- _" Ropp : R_scope.
-Notation NONA 5 "x == y == z" (eqT R x y)/\(eqT R y z) (y at level 4): R_scope.
-Notation NONA 5 "x <= y <= z" (Rle x y)/\(Rle y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <= y <  z" (Rle x y)/\(Rlt y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <  y <  z" (Rlt x y)/\(Rlt y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <  y <= z" (Rlt x y)/\(Rle y z) (y at level 4) : R_scope.
-Notation NONA 5 "x <> y"  ~(eqT R x y) : R_scope.
+Notation "x == y == z" := (eqT R x y)/\(eqT R y z)
+  (at level 5, y at level 4): R_scope.
+Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
+  (at level 5, y at level 4) : R_scope.
+Notation "x <= y < z"  := (Rle x y)/\(Rlt y z)
+  (at level 5, y at level 4) : R_scope.
+Notation  "x < y < z"  := (Rlt x y)/\(Rlt y z)
+  (at level 5, y at level 4) : R_scope.
+Notation  "x < y <= z" := (Rlt x y)/\(Rle y z)
+  (at level 5, y at level 4) : R_scope.
+Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.
 Distfix 0 "/ _" Rinv : R_scope.
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index ef9647413..760c1fc89 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -219,23 +219,34 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 Module Z_scope.
 
-Delimiters "'Z:" Z_scope "'".
-Infix 4 "+" Zplus : Z_scope.
-Infix 4 "-" Zminus : Z_scope.
-Infix 3 "*" Zmult : Z_scope.
+(* Declare Scope positive_scope with Key P. *)
+
+Delimits Scope positive_scope with P.
+Delimits Scope Z_scope with Z.
+
+Infix LEFTA 4 "+" Zplus : Z_scope.
+Infix LEFTA 4 "-" Zminus : Z_scope.
+Infix LEFTA 3 "*" Zmult : Z_scope.
 Distfix 0 "- _" Zopp : Z_scope.
-Infix NONA 5 "<=" Zle : Z_scope.
-Infix NONA 5 "<"  Zlt : Z_scope.
-Infix NONA 5 ">=" Zge : Z_scope.
+Infix 5 "<=" Zle : Z_scope.
+Infix 5 "<"  Zlt : Z_scope.
+Infix 5 ">=" Zge : Z_scope.
 (*Infix NONA 5 ">"  Zgt : Z_scope. (* Conflicts with "<..>Cases ... " *) *)
-Infix NONA 5 "?=" Zcompare : Z_scope.
-Notation NONA 5 "x <= y <= z" (Zle x y)/\(Zle y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <= y <  z" (Zle x y)/\(Zlt y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <  y <  z" (Zlt x y)/\(Zlt y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <  y <= z" (Zlt x y)/\(Zle y z) (y at level 4) : Z_scope.
-Notation NONA 5 "x <> y"      ~(eq Z x y)          : Z_scope.
-(* Notation NONA 1 "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
-Notation NONA 1 "|| x ||" (Zabs x) : Z_scope.
+Infix 5 "?=" Zcompare : Z_scope.
+Notation "x <= y <= z" := (Zle x y)/\(Zle y z)
+  (at level 5, y at level 4):Z_scope.
+Notation "x <= y < z"  := (Zle x y)/\(Zlt y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x < y <= z" := (Zlt x y)/\(Zle y z)
+  (at level 5, y at level 4):Z_scope.
+Notation  "x = y = z" := x=y/\y=z
+  (at level 5, y at level 4):Z_scope.
+
+Notation "x <> y" := ~(eq Z x y) (at level 5) : Z_scope.
+(* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
+Notation "|| x ||" := (Zabs x) (at level 1) : Z_scope.
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope Z_scope.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4da4a83bc..858add3c7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -63,7 +63,7 @@ let make_aconstr vars a =
         (idl,pat,aux rhs) in
       ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl)
   | ROrderedCase (_,b,tyopt,tm,bv) ->
-      AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -76,7 +76,7 @@ allowed in abbreviatable expressions"
   let a = aux a in
   let find_type x =
     if List.mem x !bound_binders then (x,ETIdent) else
-    if List.mem x !bound_vars then (x,ETConstr) else
+    if List.mem x !bound_vars then (x,ETConstr ((10,E),None)) else
       error ((string_of_id x)^" is unbound in the right-hand-side") in
   let typs = List.map find_type vars in
   (a, typs)
@@ -97,6 +97,8 @@ let _ = set_ast_to_rawconstr
 *)
     a)
 
+(** For old ast printer *)
+
 (* Pretty-printer state summary *)
 let _ = 
   declare_summary "syntax"
@@ -166,15 +168,17 @@ let (inGrammar, outGrammar) =
        export_function = (fun x -> Some x)}
 
 open Genarg
-let gram_define_entry (u,_ as univ) (nt,et,assoc,rl) =
+
+let check_entry_type (u,n) =
   if u = "tactic" or u = "vernac" then error "tactic and vernac not supported";
-  create_entry_if_new univ nt (entry_type_of_constr_entry_type et);
-  (nt, et, assoc, rl)
+  match entry_type (get_univ u) n with
+    | None -> Pcoq.create_entry_if_new (get_univ u) n ConstrArgType
+    | Some (ConstrArgType | IdentArgType | RefArgType) -> ()
+    | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
 
-let add_grammar_obj univ l =
+let add_grammar_obj univ entryl =
   let u = create_univ_if_new univ in
-  let entryl = List.map (gram_define_entry u) l in
-  let g = interp_grammar_command univ get_entry_type entryl in
+  let g = interp_grammar_command univ check_entry_type entryl in
   Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
 
 let add_tactic_grammar g = 
@@ -183,33 +187,49 @@ let add_tactic_grammar g =
 (* printing grammar entries *)
 let print_grammar univ entry =
   let u = get_univ univ in
-  let te = get_entry u entry in
-  Gram.Entry.print (object_of_typed_entry te)
+  let typ = explicitize_entry (fst u) entry in
+  let te,_ = entry_of_type false typ in
+  Gram.Entry.print te
 
 (* Infix, distfix, notations *)
 
+type token = WhiteSpace of int | String of string
+
 let split str =
+  let push_token beg i l =
+    if beg == i then l else String (String.sub str beg (i - beg)) :: l 
+  in
+  let push_whitespace beg i l =
+    if beg = i then l else WhiteSpace (i-beg) :: l 
+  in
   let rec loop beg i =
     if i < String.length str then
       if str.[i] == ' ' then
-        if beg == i then 
-	  loop (succ beg) (succ i)
-        else 
-	  String.sub str beg (i - beg) :: loop (succ i) (succ i)
-      else 
+	push_token beg i (loop_on_whitespace (succ i) (succ i))
+      else
 	loop beg (succ i)
-    else if beg == i then 
-      []
     else
-      [String.sub str beg (i - beg)]
+      push_token beg i []
+  and loop_on_whitespace beg i =
+    if i < String.length str then
+      if str.[i] <> ' ' then
+	push_whitespace beg i (loop i (succ i))
+      else
+	loop_on_whitespace beg (succ i)
+    else
+      push_whitespace beg i []
   in
   loop 0 0
 
 (* Build the syntax and grammar rules *)
 
+type printing_precedence = int * parenRelation
+type parsing_precedence = int option
+
 type symbol =
   | Terminal of string
-  | NonTerminal of (int * parenRelation) * identifier
+  | NonTerminal of identifier
+  | Break of int
 
 let prec_assoc = function
   | Some(Gramext.RightA) -> (L,E)
@@ -217,46 +237,67 @@ let prec_assoc = function
   | Some(Gramext.NonA) -> (L,L)
   | None -> (L,L)   (* NONA by default *)
 
-let constr_tab =
-  [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4";
-     "constr5"; "constr6"; "constr7"; "constr"; "constr9"; "lconstr";
-     "pattern" |]
-
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
-let constr_rule np = constr_tab.(level_rule np)
+(* Find the digit code of the main entry of a sub-level and its associativity
+   (i.e. [9] means "constr9", [10] means "lconstr", [11] means "pattern",
+   otherwise "constr") *)
 
-let nonterm_meta nt var x =
-  match x with
-  | ETIdent -> NonTerm(ProdPrimitive ("constr","ident"), Some (var,x))
-  | ETConstr -> NonTerm(ProdPrimitive ("constr",nt), Some (var,x))
-  | ETReference -> NonTerm(ProdPrimitive ("constr","global"), Some (var,x))
+let constr_rule = function
+  | (9|10 as n,E) -> Some n
+  | (9,L) -> None
+  | (10,L) -> Some 9
+  | (11,E) -> Some 11
+  | _ -> None
 
 (* For old ast printer *)
 let meta_pattern m = Pmeta(m,Tany)
 
+open Symbols
+
+type white_status = NextMaybeLetter | NoSpace | AddBrk of int
+
+let add_break l = function
+  | AddBrk n -> UNP_BRK (n,1) :: l
+  | _ -> l
+
+let precedence_of_entry_type = function
+  | ETConstr (prec,_) -> prec
+  | _ -> 0,E
+
 (* For old ast printer *)
-let make_hunks_ast symbols =
+let make_hunks_ast symbols etyps from =
+  let (_,l) =
   List.fold_right
-    (fun it l -> match it with
-      | NonTerminal ((_,lp),m) -> PH (meta_pattern (string_of_id m), None, lp) :: l
+    (fun it (ws,l) -> match it with
+      | NonTerminal m ->
+	  let (_,lp) = precedence_of_entry_type (List.assoc m etyps) in
+	  let u = PH (meta_pattern (string_of_id m), None, lp) in
+	  let l' = u :: (add_break l ws) in
+	  ((if from = 10 (* lconstr *) then AddBrk 1 else NextMaybeLetter), l')
       | Terminal s ->
-	  let n,s =
-	    if is_letter (s.[String.length s -1]) or is_letter (s.[0])
-	    then 1,s^" " else 0,s
-	  in
-	  UNP_BRK (n, 1) :: RO s :: l)
-    symbols []
-
-open Symbols
-
-type white_status = NextMaybeLetter | NextIsNotLetter | AddBrk of int
+	  let l' = add_break l ws in
+	  if from = 10 (* lconstr *) then (AddBrk 1, RO s :: l')
+	  else
+	    let n = if is_letter (s.[0]) then 1 else 0 in
+	    let s = 
+	      if (ws = NextMaybeLetter or ws = AddBrk 1)
+		& is_letter (s.[String.length s -1])
+	      then s^" "
+	      else s
+	    in
+	    (AddBrk n, RO s :: l')
+      | Break n ->
+	    (NoSpace, UNP_BRK (n,1) :: l))
+    symbols (NoSpace,[])
+  in l
 
-let make_hunks symbols =
+let make_hunks etyps symbols =
   let (_,l) =
   List.fold_right
     (fun it (ws,l) -> match it with
-      | NonTerminal (prec,m) ->
+      | NonTerminal m ->
+	  let prec = precedence_of_entry_type (List.assoc m etyps) in
 	  let u = UnpMetaVar (m,prec) in
 	  let l' = match ws with
 	    | AddBrk n -> UnpCut (PpBrk(n,1)) :: u :: l
@@ -270,7 +311,9 @@ let make_hunks symbols =
 	    then s^" "
 	    else s
 	  in
-	  (AddBrk n, UnpTerminal s :: l))
+	  (AddBrk n, UnpTerminal s :: l)
+      | Break n ->
+	    (NoSpace, UnpCut (PpBrk (n,1)) :: l))
     symbols (NextMaybeLetter,[])
   in l
 
@@ -278,49 +321,60 @@ let string_of_prec (n,p) =
   (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
 
 let string_of_symbol = function
-  | NonTerminal (lp,_) -> "_"
-  | Terminal s -> s
+  | NonTerminal _ -> ["_"]
+  | Terminal s -> [s]
+  | Break _ -> []
 
-let assoc_of_symbol s l = match s with
-  | NonTerminal (lp,_) -> level_rule lp :: l
-  | Terminal _ -> l
+let assoc_of_type = function
+  | (_,ETConstr (lp,_)) -> level_rule lp
+  | _ -> 0
 
 let string_of_assoc = function
   | Some(Gramext.RightA) -> "RIGHTA"
   | Some(Gramext.LeftA) | None -> "LEFTA"
   | Some(Gramext.NonA) -> "NONA"
 
-let make_symbolic assoc n symbols =
-  (n, List.fold_right assoc_of_symbol symbols []),
-  (String.concat " " (List.map string_of_symbol symbols))
-
-let make_production typs =
-  List.map (function
-    | NonTerminal (lp,m) -> nonterm_meta (constr_rule lp) m (List.assoc m typs)
-    | Terminal s -> Term (Extend.terminal s))
+let make_symbolic assoc n symbols etyps =
+  (n,List.map assoc_of_type etyps),
+  (String.concat " " (List.flatten (List.map string_of_symbol symbols)))
 
-(*
-let create_meta n = "$e"^(string_of_int n)
-*)
+let make_production etyps symbols =
+  List.fold_right
+    (fun t l -> match t with
+      | NonTerminal m ->
+	  let typ = List.assoc m etyps in
+	  NonTerm (ProdPrimitive typ, Some (m,typ)) :: l
+      | Terminal s ->
+	  Term (Extend.terminal s) :: l
+      | Break _ ->
+	  l)
+    symbols []
 
 let strip s =
   let n = String.length s in
   if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
 
-let is_symbol s = not (is_letter s.[0])
-
-let rec find_symbols c_first c_next c_last vars varprecl = function
+(* To protect alphabetic tokens from being seen as variables *)
+let quote x =
+  let n = String.length x in
+  if n > 0 &
+    (is_letter x.[0] or is_letter x.[n-1] or is_digit x.[n-1] or x.[n-1]='\'')
+  then
+    "\'"^x^"\'"
+  else
+    x
+
+let is_symbol = function String s -> not (is_letter s.[0]) | _ -> false
+
+let rec find_symbols c_first c_last vars = function
   | []    -> (vars, [])
-  | x::sl when is_letter x.[0] ->
+  | String x :: sl when is_letter x.[0] ->
       let id = Names.id_of_string x in
-      if List.mem id vars then error ("Variable "^x^" occurs more than once");
-      let prec =
-        try (List.assoc x varprecl,E)
-        with Not_found ->
-          if List.exists is_symbol sl then c_first else c_last in
-      let (vars,l) =
-        find_symbols c_next c_next c_last vars varprecl sl in
-      (id::vars, NonTerminal (prec,id) :: l)
+      if List.mem_assoc id vars then
+	error ("Variable "^x^" occurs more than once");
+      let prec = if List.exists is_symbol sl then c_first else c_last in
+      let (vars,l) = find_symbols None c_last vars sl in
+      ((id,prec)::vars, NonTerminal id :: l)
 (*
   | "_"::sl ->
       warning "Found '_'";
@@ -330,19 +384,22 @@ let rec find_symbols c_first c_next c_last vars varprecl = function
       let meta = create_meta new_var in
       (vars, NonTerminal (prec, meta) :: l)
 *)
-  | s :: sl ->
-      let (vars,l) = find_symbols c_next c_next c_last vars varprecl sl in
+  | String s :: sl ->
+      let (vars,l) = find_symbols None c_last vars sl in
       (vars, Terminal (strip s) :: l)
+  | WhiteSpace n :: sl ->
+      let (vars,l) = find_symbols c_first c_last vars sl in
+      (vars, Break n :: l)
 
-let make_grammar_rule n typs symbols ntn =
+let make_grammar_rule n assoc typs symbols ntn =
   let prod = make_production typs symbols in
-  ((if n=8 then "constr8" else constr_rule (n,E)),ntn,prod)
+  (n,assoc,ntn,prod)
 
 (* For old ast printer *)
 let metas_of sl =
   List.fold_right
     (fun it metatl -> match it with
-      | NonTerminal (_,m) -> m::metatl
+      | NonTerminal m -> m::metatl
       | _ -> metatl)
     sl []
 
@@ -352,31 +409,33 @@ let make_pattern symbols ast =
   fst (to_pat env ast)
 
 (* For old ast printer *)
-let make_syntax_rule n name symbols ast ntn sc =
+let make_syntax_rule n name symbols typs ast ntn sc =
   [{syn_id = name;
     syn_prec = n;
     syn_astpat = make_pattern symbols ast;
-    syn_hunks = [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1, make_hunks_ast symbols))]}]
+    syn_hunks =
+      [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
 
-let make_pp_rule symbols =
-  [UnpBox (PpHOVB 1, make_hunks symbols)]
+let make_pp_rule symbols typs =
+  [UnpBox (PpHOVB 1, make_hunks symbols typs)]
 
 
 (**************************************************************************)
 (* Syntax extenstion: common parsing/printing rules and no interpretation *)
 
 let cache_syntax_extension (_,(prec,ntn,gr,se)) =
-  if not (Symbols.exists_notation prec ntn) then begin
-    Egrammar.extend_grammar (Egrammar.Notation gr);
-    Symbols.declare_printing_rule ntn (se,fst prec)
-  end
+  Egrammar.extend_grammar (Egrammar.Notation gr);
+  if se<>None then
+    Symbols.declare_notation_printing_rule ntn (out_some se,fst prec)
 
 let subst_notation_grammar subst x = x
 
 let subst_printing_rule subst x = x
 
 let subst_syntax_extension (_,subst,(prec,ntn,gr,se)) =
-  (prec,ntn,subst_notation_grammar subst gr,subst_printing_rule subst se)
+  (prec,ntn,
+   subst_notation_grammar subst gr,
+   option_app (subst_printing_rule subst) se)
 
 let (inSyntaxExtension, outSyntaxExtension) =
   declare_object {(default_object "SYNTAX-EXTENSION") with
@@ -387,75 +446,100 @@ let (inSyntaxExtension, outSyntaxExtension) =
        export_function = (fun x -> Some x)}
 
 let interp_syntax_modifiers =
-  let rec interp assoc precl level etyps = function
+  let onlyparsing = ref false in
+  let rec interp assoc level etyps = function
     | [] ->
 	let n = match level with None -> 1 | Some n -> n in
-	(assoc,precl,n,etyps)
-    | SetItemLevel (id,n) :: l ->
-	if List.mem_assoc id precl then error (id^"has already a precedence")
-	else interp assoc ((id,n)::precl) level etyps l
+	(assoc,n,etyps,!onlyparsing)
+    | SetEntryType (s,typ) :: l ->
+	let id = id_of_string s in
+	if List.mem_assoc id etyps then
+	  error (s^" is already assigned to an entry or constr level")
+	else interp assoc level ((id,typ)::etyps) l
+    | SetItemLevel ([],n) :: l ->
+	interp assoc level etyps l
+    | SetItemLevel (s::idl,n) :: l ->
+	let id = id_of_string s in
+	if List.mem_assoc id etyps then
+	  error (s^" is already assigned to an entry or constr level")
+	else
+	  let typ = ETConstr ((n,E), Some n) in
+	  interp assoc level ((id,typ)::etyps) (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
-	if level <> None then error "already a level"
-	else interp assoc precl (Some n) etyps l
+	if level <> None then error "A level is mentioned more than twice"
+	else interp assoc (Some n) etyps l
     | SetAssoc a :: l ->
 	if assoc <> None then error "already an associativity"
-	else interp (Some a) precl level etyps l
-    | SetEntryType (s,typ) :: l ->
-	let id = id_of_string s in
-	if List.mem_assoc id etyps then error (s^"has already an entry type")
-	else interp assoc precl level ((id,typ)::etyps) l
-  in interp None [] None []
+	else interp (Some a) level etyps l
+    | SetOnlyParsing :: l ->
+	onlyparsing := true;
+	interp assoc level etyps l
+  in interp None None []
+
+(* 2nd list of types has priority *)
+let rec merge_entry_types etyps' = function
+  | [] -> etyps'
+  | (x,_ as e)::etyps ->
+      e :: merge_entry_types (List.remove_assoc x etyps') etyps
+
+let set_entry_type etyps (x,typ) =
+  let typ = match typ with
+  | None -> 
+      (try List.assoc x etyps
+      with Not_found -> ETConstr ((10,E), Some 10))
+  | Some typ ->
+      let typ = ETConstr (typ,constr_rule typ) in
+      try List.assoc x etyps
+      with Not_found -> typ in
+  (x,typ)
 
 let add_syntax_extension df modifiers =
-  let (assoc,varprecl,n,etyps) = interp_syntax_modifiers modifiers in
+  let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
   let (lp,rp) = prec_assoc assoc in
-  let (ids,symbs) = find_symbols (n,lp) (10,E) (n,rp) [] varprecl (split df) in
-  let (prec,notation) = make_symbolic assoc n symbs in
-  let gram_rule = make_grammar_rule n etyps symbs notation in
-  let pp_rule = make_pp_rule symbs in
-  Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
+  let (typs,symbs) = find_symbols (Some (n,lp)) (Some (n,rp)) [] (split df) in
+  let typs = List.map (set_entry_type etyps) typs in
+  let (prec,notation) = make_symbolic assoc n symbs typs in
+  let gram_rule = make_grammar_rule n assoc typs symbs notation in
+  let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in
+  if not (Symbols.exists_notation prec notation) then
+    Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
 
 (**********************************************************************)
 (* Distfix, Infix, Notations *)
 
 (* A notation comes with a grammar rule, a pretty-printing rule, an
    identifiying pattern called notation and an associated scope *)
-let load_infix _ (_,(gr,_,se,prec,ntn,scope,pat)) =
+let load_notation _ (_,(_,prec,ntn,scope,_,pat,onlyparse,_)) =
   Symbols.declare_scope scope
 
-let open_infix i (_,(gr,oldse,se,prec,ntn,scope,pat)) =
+let open_notation i (_,(oldse,prec,ntn,scope,metas,pat,onlyparse,df)) =
   if i=1 then begin
     let b = Symbols.exists_notation_in_scope scope prec ntn pat in
-    (* Declare the printer rule and its interpretation *)
-    if not b then Esyntax.add_ppobject {sc_univ="constr";sc_entries=oldse};
-    (* Declare the grammar and printing rules ... *)
-    if not (Symbols.exists_notation prec ntn) then begin
-      Egrammar.extend_grammar (Egrammar.Notation gr);
-      Symbols.declare_printing_rule ntn (se,fst prec)
-    end;
-    (* ... and their interpretation *)
+    (* Declare the old printer rule and its interpretation *)
+    if not b & oldse <> None then
+      Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse};
+    (* Declare the interpretation *)
     if not b then
-      Symbols.declare_notation ntn scope (pat,prec);
+      Symbols.declare_notation ntn scope (metas,pat) prec df onlyparse;
   end
 
-let cache_infix o =
-  load_infix 1 o;
-  open_infix 1 o
+let cache_notation o =
+  load_notation 1 o;
+  open_notation 1 o
 
-let subst_infix (_,subst,(gr,oldse,se,prec,ntn,scope,pat)) =
-  (subst_notation_grammar subst gr,
-   list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) oldse,
-   subst_printing_rule subst se,
+let subst_notation (_,subst,(oldse,prec,ntn,scope,metas,pat,b,df)) =
+  (option_app
+    (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse,
    prec,ntn,
    scope,
-   subst_aconstr subst pat)
-
-let (inInfix, outInfix) =
-  declare_object {(default_object "INFIX") with
-       open_function = open_infix;
-       cache_function = cache_infix;
-       subst_function = subst_infix;
-       load_function = load_infix;
+   metas,subst_aconstr subst pat, b, df)
+
+let (inNotation, outNotation) =
+  declare_object {(default_object "NOTATION") with
+       open_function = open_notation;
+       cache_function = cache_notation;
+       subst_function = subst_notation;
+       load_function = load_notation;
        classify_function = (fun (_,o) -> Substitute o);
        export_function = (fun x -> Some x)}
 
@@ -473,56 +557,71 @@ let rec reify_meta_ast vars = function
   | Dynamic _ as a -> (* Hum... what to do here *) a
 
 (* For old ast syntax *)
-let make_old_pp_rule n symbols r ntn scope vars =
+let make_old_pp_rule n symbols typs r ntn scope vars =
   let ast = Termast.ast_of_rawconstr r in
   let ast = reify_meta_ast vars ast in
   let rule_name = ntn^"_"^scope^"_notation" in
-  make_syntax_rule n rule_name symbols ast ntn scope
-
-let add_notation df ast modifiers sc =
-  let (assoc,varprecl,n,_) = interp_syntax_modifiers modifiers in
+  make_syntax_rule n rule_name symbols typs ast ntn scope
+
+let add_notation df a modifiers sc =
+  let toks = split df in
+  let (assoc,n,etyps,onlyparse) =
+    if modifiers = [] &
+      match toks with [String x] when quote(strip x) = x -> true | _ -> false
+    then
+      (* Means a Syntactic Definition *)
+      (None,0,[],false)
+    else
+      interp_syntax_modifiers modifiers
+  in
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
   let (lp,rp) = prec_assoc assoc in
-  let (vars,symbols) =
-    find_symbols (n,lp) (10,E) (n,rp) [] varprecl (split df) in
-  let (prec,notation) = make_symbolic assoc n symbols in
+  let (typs,symbols) = find_symbols (Some (n,lp)) (Some (n,rp)) [] toks in
+  let vars = List.map fst typs in
   (* To globalize... *)
-  let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars ast in
-  let a,typs = make_aconstr vars r in
-  let typs =
-    List.map (fun (x,t) -> 
-      (x,if List.mem_assoc (string_of_id x) varprecl then ETConstr else t))
-      typs
-  in
-  let gram_rule = make_grammar_rule n typs symbols notation in
-  let pp_rule = make_pp_rule symbols in
-  let old_pp_rule = make_old_pp_rule n symbols r notation scope vars in
-  Lib.add_anonymous_leaf (inInfix(gram_rule,old_pp_rule,pp_rule,prec,notation,scope,a))
+  let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars a in
+  let a,_ = make_aconstr vars r in
+(*
+  let a,etyps' = make_aconstr vars r in
+  let etyps = merge_entry_types etyps' etyps in
+*)
+  let typs = List.map (set_entry_type etyps) typs in
+  (* Declare the parsing and printing rules if not already done *)
+  let (prec,notation) = make_symbolic assoc n symbols typs in
+  let gram_rule = make_grammar_rule n assoc typs symbols notation in
+  let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbols) in
+  if not (Symbols.exists_notation prec notation) then
+  Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule));
+  let old_pp_rule =
+    if onlyparse then None
+    else Some (make_old_pp_rule n symbols typs r notation scope vars) in
+  (* Declare the interpretation *)
+  Lib.add_anonymous_leaf
+    (inNotation(old_pp_rule,prec,notation,scope,vars,a,onlyparse,df))
 
 (* TODO add boxes information in the expression *)
 
 let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
 
-(* To protect alphabetic tokens from being seen as variables *)
-let quote x = "\'"^x^"\'"
-
 let rec rename x vars n = function
   | [] ->
       (vars,[])
-  | "_"::l ->
+  | String "_"::l ->
       let (vars,l) = rename x vars (n+1) l in
       let xn = x^(string_of_int n) in
       ((inject_var xn)::vars,xn::l)
-  | y::l ->
+  | String y::l ->
       let (vars,l) = rename x vars n l in (vars,(quote y)::l)
+  | WhiteSpace _::l ->
+      rename x vars n l
 
 let add_distfix assoc n df r sc =
-  (* "x" cannot clash since ast is globalized (included section vars) *)
+  (* "x" cannot clash since r is globalized (included section vars) *)
   let (vars,l) = rename "x" [] 1 (split df) in
   let df = String.concat " " l in
-  let ast = mkAppC (mkRefC r, vars) in
-  let a = match assoc with None -> Gramext.LeftA | Some a -> a in
-  add_notation df ast [SetAssoc a;SetLevel n] sc
+  let a = mkAppC (mkRefC r, vars) in
+  let assoc = match assoc with None -> [] | Some a -> [SetAssoc a] in
+  add_notation df a (SetLevel n :: assoc) sc
 
 let add_infix assoc n inf pr sc =
 (*  let pr = Astterm.globalize_qualid pr in*)
@@ -536,9 +635,9 @@ let add_infix assoc n inf pr sc =
       (str"Associativity Precedence must be 6,7,8 or 9.");
   *)
   let metas = [inject_var "x"; inject_var "y"] in
-  let ast = mkAppC (mkRefC pr,metas) in
-  let a = match assoc with None -> Gramext.LeftA | Some a -> a in
-  add_notation ("x "^(quote inf)^" y") ast [SetAssoc a;SetLevel n] sc
+  let a = mkAppC (mkRefC pr,metas) in
+  let assoc = match assoc with None -> [] | Some a -> [SetAssoc a] in
+  add_notation ("x "^(quote inf)^" y") a (SetLevel n :: assoc) sc
 
 (* Delimiters *)
 let load_delimiters _ (_,(_,_,scope,dlm)) =
@@ -563,13 +662,13 @@ let (inDelim,outDelim) =
       load_function = load_delimiters;
       export_function = (fun x -> Some x) }
 
-let make_delimiter_rule (l,r) inlevel =
+let make_delimiter_rule (l,r) typ =
   let e = Nameops.make_ident "e" None in
-  let symbols = [Terminal l; NonTerminal ((inlevel,E),e); Terminal r] in
-  make_production [e,ETConstr] symbols
+  let symbols = [Terminal l; NonTerminal e; Terminal r] in
+  make_production [e,typ] symbols
 
 let add_delimiters scope (l,r as dlms) =
   if l = "" or r = "" then error "Delimiters cannot be empty";
-  let gram_rule = make_delimiter_rule dlms 0 (* constr0 *) in
-  let pat_gram_rule = make_delimiter_rule dlms 11 (* "pattern" *) in
+  let gram_rule = make_delimiter_rule dlms (ETConstr ((0,E),Some 0)) in
+  let pat_gram_rule = make_delimiter_rule dlms ETPattern in
   Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms))
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0506dd2da..35ef1e620 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -42,7 +42,8 @@ type pcoq_hook = {
   search : searchable -> dir_path list * bool -> unit;
   print_name : reference -> unit;
   print_check : Environ.unsafe_judgment -> unit;
-  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit;
+  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> 
+    Environ.unsafe_judgment -> unit;
   show_goal : int option -> unit
 }
 
@@ -783,6 +784,7 @@ let vernac_print = function
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintHintDb -> Auto.print_searchtable ()
+  | PrintScope s -> pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
 
 let global_loaded_library r =
   let (loc,qid) = qualid_of_reference r in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index be0f4d678..050ac58d1 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -56,6 +56,7 @@ type printable =
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintHintDb
+  | PrintScope of string
 
 type searchable =
   | SearchPattern of pattern_expr