Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; hack temporaire autour du printer

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

29 files changed, 1666 insertions, 689 deletions

diff --git a/.depend b/.depend
index 1de0955e5d..fa54784eab 100644
--- a/.depend
+++ b/.depend
@@ -15,10 +15,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi 
 kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/names.cmi kernel/univ.cmi 
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -37,9 +37,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/entries.cmi kernel/indtypes.cmi library/libnames.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
@@ -67,31 +64,38 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/util.cmi 
 library/summary.cmi: library/libnames.cmi kernel/names.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
-    library/libnames.cmi kernel/names.cmi lib/pp.cmi proofs/tacexpr.cmo \
-    lib/util.cmi 
+    library/libnames.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi 
 parsing/astmod.cmi: parsing/coqast.cmi kernel/declarations.cmi \
     kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi 
+parsing/astterm2.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
+    library/impargs.cmi library/libnames.cmi kernel/names.cmi \
+    pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    kernel/term.cmi lib/util.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/impargs.cmi library/libnames.cmi kernel/names.cmi \
     pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     kernel/term.cmi lib/util.cmi 
-parsing/coqast.cmi: lib/dyn.cmi library/libnames.cmi kernel/names.cmi 
+parsing/coqast.cmi: lib/bignat.cmi lib/dyn.cmi library/libnames.cmi \
+    kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi 
 parsing/coqlib.cmi: library/libnames.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi kernel/term.cmi 
 parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     parsing/genarg.cmi kernel/names.cmi proofs/tacexpr.cmo \
     toplevel/vernacexpr.cmo 
 parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
-    library/libnames.cmi lib/pp.cmi toplevel/vernacexpr.cmo 
-parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi library/libnames.cmi \
-    kernel/names.cmi lib/pp.cmi 
-parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/term.cmi 
-parsing/g_zsyntax.cmi: parsing/coqast.cmi 
+    parsing/genarg.cmi lib/pp.cmi parsing/symbols.cmi toplevel/vernacexpr.cmo 
+parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
+    lib/pp.cmi 
 parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/term.cmi lib/util.cmi 
+parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/term.cmi 
+parsing/g_zsyntax.cmi: parsing/coqast.cmi 
 parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -112,6 +116,8 @@ parsing/printer.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \
 parsing/printmod.cmi: kernel/names.cmi lib/pp.cmi 
 parsing/search.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi 
+parsing/symbols.cmi: lib/bignat.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/rawterm.cmi lib/util.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi \
     library/libnames.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
@@ -275,7 +281,7 @@ toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \
     kernel/indtypes.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi kernel/type_errors.cmi 
 toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi \
-    library/libnames.cmi proofs/tacexpr.cmo lib/util.cmi \
+    library/libnames.cmi parsing/symbols.cmi proofs/tacexpr.cmo lib/util.cmi \
     toplevel/vernacexpr.cmo 
 toplevel/mltop.cmi: library/libobject.cmi kernel/names.cmi 
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
@@ -285,21 +291,21 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/proof_type.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernacexpr.cmo 
 contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi 
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
     contrib/correctness/ptype.cmi kernel/term.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -449,6 +455,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \
+    lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \
+    lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -457,12 +469,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \
-    lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \
-    lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -533,6 +539,8 @@ kernel/univ.cmo: lib/hashcons.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     kernel/univ.cmi 
 kernel/univ.cmx: lib/hashcons.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     kernel/univ.cmi 
+lib/bignat.cmo: lib/bignat.cmi 
+lib/bignat.cmx: lib/bignat.cmi 
 lib/bij.cmo: lib/gmap.cmi lib/bij.cmi 
 lib/bij.cmx: lib/gmap.cmx lib/bij.cmi 
 lib/bstack.cmo: lib/util.cmi lib/bstack.cmi 
@@ -543,34 +551,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi library/global.cmi library/impargs.cmi \
     kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \
@@ -663,6 +661,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/argextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -670,39 +678,63 @@ parsing/argextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
     parsing/q_coqast.cmx parsing/q_util.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
-    library/libnames.cmi kernel/names.cmi lib/pp.cmi proofs/tacexpr.cmo \
-    lib/util.cmi parsing/ast.cmi 
+    library/libnames.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
+    parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \
-    library/libnames.cmx kernel/names.cmx lib/pp.cmx proofs/tacexpr.cmx \
-    lib/util.cmx parsing/ast.cmi 
+    library/libnames.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
+    parsing/ast.cmi 
 parsing/astmod.cmo: parsing/astterm.cmi parsing/coqast.cmi kernel/entries.cmi \
     pretyping/evd.cmi library/libnames.cmi kernel/modops.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/astmod.cmi 
 parsing/astmod.cmx: parsing/astterm.cmx parsing/coqast.cmx kernel/entries.cmx \
     pretyping/evd.cmx library/libnames.cmx kernel/modops.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx lib/util.cmx parsing/astmod.cmi 
-parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
+parsing/astterm2.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     library/global.cmi library/impargs.cmi library/libnames.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
     pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
     pretyping/pretyping.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
-    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
-    pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
-parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
+    pretyping/retyping.cmi kernel/sign.cmi parsing/symbols.cmi \
+    pretyping/syntax_def.cmi kernel/term.cmi parsing/termast.cmi \
+    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    parsing/astterm2.cmi 
+parsing/astterm2.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     lib/dyn.cmx kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
     library/global.cmx library/impargs.cmx library/libnames.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
     pretyping/pretyping.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx parsing/symbols.cmx \
+    pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx \
+    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    parsing/astterm2.cmi 
+parsing/astterm.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
+    library/declare.cmi lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+    pretyping/evd.cmi library/global.cmi library/impargs.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi pretyping/pretyping.cmi \
+    pretyping/rawterm.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+    kernel/sign.cmi parsing/symbols.cmi pretyping/syntax_def.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
+    pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
+parsing/astterm.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
+    library/declare.cmx lib/dyn.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    pretyping/evd.cmx library/global.cmx library/impargs.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx pretyping/pretyping.cmx \
+    pretyping/rawterm.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+    kernel/sign.cmx parsing/symbols.cmx pretyping/syntax_def.cmx \
     kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
     pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi 
-parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi library/libnames.cmi \
-    kernel/names.cmi lib/util.cmi parsing/coqast.cmi 
-parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx library/libnames.cmx \
-    kernel/names.cmx lib/util.cmx parsing/coqast.cmi 
+parsing/coqast.cmo: lib/bignat.cmi lib/dyn.cmi lib/hashcons.cmi \
+    library/libnames.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi lib/util.cmi parsing/coqast.cmi 
+parsing/coqast.cmx: lib/bignat.cmx lib/dyn.cmx lib/hashcons.cmx \
+    library/libnames.cmx kernel/names.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    kernel/term.cmx lib/util.cmx parsing/coqast.cmi 
 parsing/coqlib.cmo: library/declare.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi kernel/term.cmi lib/util.cmi \
     parsing/coqlib.cmi 
@@ -720,17 +752,17 @@ parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     parsing/genarg.cmi lib/gmap.cmi lib/gmapl.cmi library/libnames.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo parsing/esyntax.cmi 
+    parsing/symbols.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    parsing/esyntax.cmi 
 parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
     parsing/genarg.cmx lib/gmap.cmx lib/gmapl.cmx library/libnames.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx parsing/esyntax.cmi 
+    parsing/symbols.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    parsing/esyntax.cmi 
 parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
-    parsing/lexer.cmi library/libnames.cmi lib/pp.cmi lib/util.cmi \
-    parsing/extend.cmi 
+    parsing/lexer.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
 parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \
-    parsing/lexer.cmx library/libnames.cmx lib/pp.cmx lib/util.cmx \
-    parsing/extend.cmi 
+    parsing/lexer.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
 parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/extend.cmi library/goptions.cmi parsing/pcoq.cmi lib/pp.cmi \
     toplevel/vernacexpr.cmo 
@@ -745,6 +777,12 @@ parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \
     parsing/pcoq.cmx 
+parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
+    parsing/genarg.cmi 
+parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
+    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
+    parsing/genarg.cmi 
 parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -761,28 +799,34 @@ parsing/g_module.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi 
 parsing/g_module.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx 
-parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
+parsing/g_natsyntax.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
     parsing/coqlib.cmi parsing/esyntax.cmi parsing/extend.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi parsing/termast.cmi \
+    library/libnames.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+    lib/pp.cmi pretyping/rawterm.cmi parsing/symbols.cmi parsing/termast.cmi \
     lib/util.cmi parsing/g_natsyntax.cmi 
-parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
+parsing/g_natsyntax.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     parsing/coqlib.cmx parsing/esyntax.cmx parsing/extend.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx parsing/termast.cmx \
+    library/libnames.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+    lib/pp.cmx pretyping/rawterm.cmx parsing/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 proofs/tacexpr.cmo 
+    library/nametab.cmi parsing/pcoq.cmi 
 parsing/g_prim.cmx: parsing/coqast.cmx library/libnames.cmx kernel/names.cmx \
-    library/nametab.cmx parsing/pcoq.cmx proofs/tacexpr.cmx 
+    library/nametab.cmx parsing/pcoq.cmx 
 parsing/g_proofs.cmo: parsing/coqast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
     lib/pp.cmi proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
 parsing/g_proofs.cmx: parsing/coqast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
     lib/pp.cmx proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx 
-parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
-    parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi 
-parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx 
+parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi lib/bignat.cmi \
+    parsing/coqast.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    library/libnames.cmi library/library.cmi kernel/names.cmi lib/options.cmi \
+    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi parsing/symbols.cmi \
+    lib/util.cmi 
+parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx lib/bignat.cmx \
+    parsing/coqast.cmx parsing/esyntax.cmx parsing/extend.cmx \
+    library/libnames.cmx library/library.cmx kernel/names.cmx lib/options.cmx \
+    parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/symbols.cmx \
+    lib/util.cmx 
 parsing/g_tactic.cmo: parsing/ast.cmi parsing/genarg.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
     lib/util.cmi 
@@ -797,18 +841,16 @@ parsing/g_vernac.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \
     library/declare.cmx parsing/genarg.cmx library/goptions.cmx \
     library/libnames.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
     toplevel/recordobj.cmx lib/util.cmx toplevel/vernacexpr.cmx 
-parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
-    parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi parsing/g_zsyntax.cmi 
-parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx parsing/g_zsyntax.cmi 
-parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
-    parsing/genarg.cmi 
-parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
-    parsing/genarg.cmi 
+parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi lib/bignat.cmi \
+    parsing/coqast.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    library/libnames.cmi library/library.cmi kernel/names.cmi \
+    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi parsing/symbols.cmi \
+    lib/util.cmi parsing/g_zsyntax.cmi 
+parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx lib/bignat.cmx \
+    parsing/coqast.cmx parsing/esyntax.cmx parsing/extend.cmx \
+    library/libnames.cmx library/library.cmx kernel/names.cmx \
+    parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/symbols.cmx \
+    lib/util.cmx parsing/g_zsyntax.cmi 
 parsing/lexer.cmo: parsing/lexer.cmi 
 parsing/lexer.cmx: parsing/lexer.cmi 
 parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
@@ -827,16 +869,16 @@ parsing/ppconstr.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/termast.cmx \
     lib/util.cmx parsing/ppconstr.cmi 
-parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
-    parsing/extend.cmi parsing/genarg.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/ppconstr.cmi \
-    parsing/printer.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \
-    parsing/pptactic.cmi 
-parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \
-    parsing/extend.cmx parsing/genarg.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/ppconstr.cmx \
-    parsing/printer.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx lib/util.cmx \
-    parsing/pptactic.cmi 
+parsing/pptactic.cmo: kernel/closure.cmi parsing/coqast.cmi lib/dyn.cmi \
+    parsing/egrammar.cmi parsing/extend.cmi parsing/genarg.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/ppconstr.cmi parsing/printer.cmi pretyping/rawterm.cmi \
+    proofs/tacexpr.cmo lib/util.cmi parsing/pptactic.cmi 
+parsing/pptactic.cmx: kernel/closure.cmx parsing/coqast.cmx lib/dyn.cmx \
+    parsing/egrammar.cmx parsing/extend.cmx parsing/genarg.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/ppconstr.cmx parsing/printer.cmx pretyping/rawterm.cmx \
+    proofs/tacexpr.cmx lib/util.cmx parsing/pptactic.cmi 
 parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -897,6 +939,14 @@ parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx parsing/coqlib.cmx \
     pretyping/pattern.cmx lib/pp.cmx pretyping/pretyping.cmx \
     parsing/printer.cmx pretyping/rawterm.cmx pretyping/retyping.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/search.cmi 
+parsing/symbols.cmo: lib/bignat.cmi parsing/coqast.cmi library/lib.cmi \
+    library/libobject.cmi kernel/names.cmi library/nametab.cmi \
+    lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi \
+    lib/util.cmi parsing/symbols.cmi 
+parsing/symbols.cmx: lib/bignat.cmx parsing/coqast.cmx library/lib.cmx \
+    library/libobject.cmx kernel/names.cmx library/nametab.cmx \
+    lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx library/summary.cmx \
+    lib/util.cmx parsing/symbols.cmi 
 parsing/tacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/pp_control.cmi parsing/q_coqast.cmo parsing/q_util.cmi \
     lib/util.cmi toplevel/vernacexpr.cmo 
@@ -925,6 +975,22 @@ parsing/vernacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
 parsing/vernacextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx parsing/q_util.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx 
+pretyping/cases2.cmo: pretyping/coercion.cmi kernel/declarations.cmi \
+    kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
+    library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
+    library/nameops.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi \
+    kernel/typeops.cmi lib/util.cmi 
+pretyping/cases2.cmx: pretyping/coercion.cmx kernel/declarations.cmx \
+    kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \
+    library/global.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
+    library/nameops.cmx kernel/names.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx pretyping/rawterm.cmx \
+    pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \
+    kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \
+    kernel/typeops.cmx lib/util.cmx 
 pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
     library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
@@ -1657,10 +1723,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
     kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1781,16 +1847,20 @@ toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi
 toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi 
 toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \
-    parsing/extend.cmi parsing/genarg.cmi library/global.cmi library/lib.cmi \
+    pretyping/evd.cmi parsing/extend.cmi parsing/genarg.cmi \
+    library/global.cmi library/impargs.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi library/library.cmi \
-    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi library/summary.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo toplevel/metasyntax.cmi 
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    library/summary.cmi parsing/symbols.cmi parsing/termast.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/metasyntax.cmi 
 toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \
-    parsing/extend.cmx parsing/genarg.cmx library/global.cmx library/lib.cmx \
+    pretyping/evd.cmx parsing/extend.cmx parsing/genarg.cmx \
+    library/global.cmx library/impargs.cmx library/lib.cmx \
     library/libnames.cmx library/libobject.cmx library/library.cmx \
-    library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx library/summary.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx toplevel/metasyntax.cmi 
+    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    library/summary.cmx parsing/symbols.cmx parsing/termast.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/metasyntax.cmi 
 toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
     parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
@@ -1853,16 +1923,6 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
-    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
-    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    lib/pp.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: parsing/ast.cmi parsing/astmod.cmi \
     parsing/astterm.cmi tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \
@@ -1877,11 +1937,11 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astmod.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 \
-    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 kernel/typeops.cmi kernel/univ.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
-    toplevel/vernacentries.cmi 
+    parsing/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 \
+    kernel/typeops.cmi kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astmod.cmx \
     parsing/astterm.cmx tactics/auto.cmx toplevel/class.cmx \
     pretyping/classops.cmx toplevel/command.cmx parsing/coqast.cmx \
@@ -1896,19 +1956,19 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astmod.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 \
-    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 kernel/typeops.cmx kernel/univ.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernacentries.cmi 
+    parsing/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 \
+    kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacexpr.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/extend.cmi parsing/genarg.cmi library/goptions.cmi \
     library/libnames.cmi kernel/names.cmi library/nametab.cmi \
-    proofs/proof_type.cmi proofs/tacexpr.cmo lib/util.cmi 
+    proofs/proof_type.cmi parsing/symbols.cmi proofs/tacexpr.cmo lib/util.cmi 
 toplevel/vernacexpr.cmx: parsing/ast.cmx parsing/coqast.cmx \
     parsing/extend.cmx parsing/genarg.cmx library/goptions.cmx \
     library/libnames.cmx kernel/names.cmx library/nametab.cmx \
-    proofs/proof_type.cmx proofs/tacexpr.cmx lib/util.cmx 
+    proofs/proof_type.cmx parsing/symbols.cmx proofs/tacexpr.cmx lib/util.cmx 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/extend.cmi toplevel/himsg.cmi library/libnames.cmi \
     kernel/names.cmi lib/options.cmi lib/pp.cmi proofs/proof_type.cmi \
@@ -1919,6 +1979,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
     proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
 contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -1941,6 +2011,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     proofs/proof_type.cmx proofs/refiner.cmx tactics/tacinterp.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
     library/declare.cmi pretyping/detyping.cmi kernel/entries.cmi \
     library/global.cmi kernel/indtypes.cmi library/libnames.cmi \
@@ -1955,18 +2037,6 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
     contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2503,6 +2573,14 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
     proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \
@@ -2527,14 +2605,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2703,8 +2773,6 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
     library/declaremods.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi library/lib.cmi library/libnames.cmi \
@@ -2731,6 +2799,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/.depend.coq b/.depend.coq
index 0be89ef685..98d6edb797 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,206 +1,206 @@
-theories/Init/Datatypes.vo: theories/Init/Datatypes.v
-theories/Init/Peano.vo: theories/Init/Peano.v
-theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v
-theories/Init/Prelude.vo: theories/Init/Prelude.v
-theories/Init/Logic.vo: theories/Init/Logic.v
-theories/Init/Specif.vo: theories/Init/Specif.v
-theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v
-theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v
-theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v
-theories/Init/Wf.vo: theories/Init/Wf.v
-theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v
-theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v
-theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v
-theories/Logic/Classical.vo: theories/Logic/Classical.v
-theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v
-theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v
-theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
-theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v
-theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
-theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v
-theories/Logic/Berardi.vo: theories/Logic/Berardi.v
-theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
-theories/Logic/Decidable.vo: theories/Logic/Decidable.v
-theories/Logic/JMeq.vo: theories/Logic/JMeq.v
-theories/Arith/ArithSyntax.vo: theories/Arith/ArithSyntax.v
-theories/Arith/Arith.vo: theories/Arith/Arith.v
-theories/Arith/Gt.vo: theories/Arith/Gt.v
-theories/Arith/Between.vo: theories/Arith/Between.v
-theories/Arith/Le.vo: theories/Arith/Le.v
-theories/Arith/Compare.vo: theories/Arith/Compare.v
-theories/Arith/Lt.vo: theories/Arith/Lt.v
-theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v
-theories/Arith/Min.vo: theories/Arith/Min.v
-theories/Arith/Div2.vo: theories/Arith/Div2.v
-theories/Arith/Minus.vo: theories/Arith/Minus.v
-theories/Arith/Mult.vo: theories/Arith/Mult.v
-theories/Arith/Even.vo: theories/Arith/Even.v
-theories/Arith/EqNat.vo: theories/Arith/EqNat.v
-theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v
-theories/Arith/Euclid.vo: theories/Arith/Euclid.v
-theories/Arith/Plus.vo: theories/Arith/Plus.v
-theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v
-theories/Arith/Max.vo: theories/Arith/Max.v
-theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v
-theories/Bool/Bool.vo: theories/Bool/Bool.v
-theories/Bool/IfProp.vo: theories/Bool/IfProp.v
-theories/Bool/Zerob.vo: theories/Bool/Zerob.v
-theories/Bool/DecBool.vo: theories/Bool/DecBool.v
-theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
-theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v
-theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v
-theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v
-theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v
-theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v
-theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v
-theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v
-theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v
-theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v
-theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v
-theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v
-theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v
-theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v
-theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v
-theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v
-theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v
-theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v
-theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v
-theories/Lists/List.vo: theories/Lists/List.v
-theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v
-theories/Lists/ListSet.vo: theories/Lists/ListSet.v
-theories/Lists/Streams.vo: theories/Lists/Streams.v
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v
-theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v
-theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v
-theories/Sets/Permut.vo: theories/Sets/Permut.v
-theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v
-theories/Sets/Powerset.vo: theories/Sets/Powerset.v
-theories/Sets/Cpo.vo: theories/Sets/Cpo.v
-theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v
-theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
-theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v
-theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v
-theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
-theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v
-theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v
-theories/Sets/Image.vo: theories/Sets/Image.v
-theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v
-theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v
-theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v
-theories/Sets/Integers.vo: theories/Sets/Integers.v
-theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v
-theories/Sets/Multiset.vo: theories/Sets/Multiset.v
-theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v
-theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v
-theories/Sets/Uniset.vo: theories/Sets/Uniset.v
-theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v
-theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v
-theories/IntMap/Addec.vo: theories/IntMap/Addec.v
-theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v
-theories/IntMap/Addr.vo: theories/IntMap/Addr.v
-theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v
-theories/IntMap/Adist.vo: theories/IntMap/Adist.v
-theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v
-theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v
-theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v
-theories/IntMap/Fset.vo: theories/IntMap/Fset.v
-theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v
-theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v
-theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v
-theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v
-theories/IntMap/Map.vo: theories/IntMap/Map.v
-theories/Relations/Newman.vo: theories/Relations/Newman.v
-theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v
-theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
-theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v
-theories/Relations/Relations.vo: theories/Relations/Relations.v
-theories/Relations/Rstar.vo: theories/Relations/Rstar.v
-theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v
-theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v
-theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v
-theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v
-theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v
-theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v
-theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v
-theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v
-theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v
-theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
-theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v
-theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v
-theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v
-theories/Reals/Rbase.vo: theories/Reals/Rbase.v
-theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v
-theories/Reals/Binome.vo: theories/Reals/Binome.v
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v
-theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v
-theories/Reals/Alembert_compl.vo: theories/Reals/Alembert_compl.v
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v
-theories/Reals/Cv_prop.vo: theories/Reals/Cv_prop.v
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v
-theories/Reals/TAF.vo: theories/Reals/TAF.v
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v
-theories/Reals/Reals.vo: theories/Reals/Reals.v
-theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
-theories/Sorting/Heap.vo: theories/Sorting/Heap.v
-theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v
-theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v
-contrib/omega/Omega.vo: contrib/omega/Omega.v
-contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v
-contrib/romega/ROmega.vo: contrib/romega/ROmega.v
-contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v
-contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v
-contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v
-contrib/ring/Ring.vo: contrib/ring/Ring.v
-contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v
-contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v
-contrib/ring/Quote.vo: contrib/ring/Quote.v
-contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v
-contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v
-contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v
-contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
-contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v
-contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v
-contrib/field/Field.vo: contrib/field/Field.v
-contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v
-contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v
-contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v
-contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v
-contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v
-contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v
-contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
-contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v
-contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v
+contrib/cc/CC.vo: contrib/cc/CC.v theories/Logic/Eqdep_dec.vo
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v
-contrib/cc/CC.vo: contrib/cc/CC.v
+contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo
+contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
+contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
+contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo
+contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/ZArith/ZArith.vo theories/Arith/Bool_nat.vo theories/Bool/Sumbool.vo
+contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
+contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo theories/ZArith/Zwf.vo contrib/correctness/Arrays.vo
+contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
+contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
+contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
+contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
+contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
+contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo
+contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/Quote.vo: contrib/ring/Quote.v
+contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
+contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
+contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
+contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
+contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo theories/Arith/Minus.vo
+theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
+theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
+theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
+theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Rpower.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert_compl.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Ranalysis.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/DiscrR.vo theories/Reals/SplitRmult.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/AltSeries.vo theories/Reals/Rcomplet.vo theories/Reals/Rprod.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Sqrt_reg.vo
+theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rderiv.vo theories/Reals/R_sqr.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
+theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
+theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
+theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rsqrt_def.vo
+theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cv_prop.vo theories/Reals/Ranalysis1.vo
+theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
+theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo theories/Reals/Binome.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
+theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rsigma.vo theories/Reals/Alembert.vo theories/Reals/Alembert_compl.vo theories/Reals/Binome.vo theories/Reals/Cv_prop.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
+theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rlimit.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
+theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/DiscrR.vo theories/Reals/Rderiv.vo theories/Reals/Alembert.vo theories/Reals/Ranalysis1.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
+theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/DiscrR.vo theories/Reals/Rtrigo.vo
+theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_sqr.vo theories/Reals/Rfunctions.vo theories/Reals/Rsigma.vo theories/Reals/Rlimit.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_plus.vo
+theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rprod.vo theories/Reals/Cv_prop.vo theories/Reals/Cos_rel.vo
+theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cauchy_prod.vo
+theories/Reals/Cv_prop.vo: theories/Reals/Cv_prop.v theories/Arith/Max.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/AltSeries.vo
+theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
+theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Binome.vo theories/Reals/Rcomplet.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo theories/Reals/AltSeries.vo
+theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Arith/Even.vo theories/Arith/Div2.vo theories/Arith/Max.vo theories/Reals/DiscrR.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Rcomplet.vo theories/Reals/Binome.vo
+theories/Reals/Alembert_compl.vo: theories/Reals/Alembert_compl.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Reals/Alembert.vo
+theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo
+theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Alembert.vo theories/Reals/Binome.vo
+theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Alembert.vo
+theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Arith/Max.vo theories/Reals/Raxioms.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
+theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
+theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
+theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
+theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
+theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo theories/Reals/Rbase.vo contrib/fourier/Fourier.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
+theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
+theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
+theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo
+theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
+theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
+theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theories/Logic/Eqdep.vo
+theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo
+theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo
+theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
+theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
+theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v
+theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo
+theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo
+theories/Relations/Rstar.vo: theories/Relations/Rstar.v
+theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo
+theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo
+theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
+theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
+theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
+theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo
+theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
+theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo
+theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo
+theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
+theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo
+theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo
+theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo
+theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo
+theories/IntMap/Adist.vo: theories/IntMap/Adist.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/Arith/Min.vo theories/IntMap/Addr.vo
+theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
+theories/IntMap/Addr.vo: theories/IntMap/Addr.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo
+theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
+theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo
+theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
+theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
+theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
+theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
+theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
+theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
+theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
+theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
+theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
+theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
+theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
+theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
+theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
+theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
+theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
+theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
+theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
+theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
+theories/Sets/Permut.vo: theories/Sets/Permut.v
+theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
+theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
+theories/Lists/Streams.vo: theories/Lists/Streams.v
+theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
+theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
+theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/ZArith_base.vo theories/Bool/Sumbool.vo
+theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
+theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo contrib/omega/Omega.vo
+theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith_base.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
+theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
+theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo
+theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo
+theories/ZArith/fast_integer.vo: theories/ZArith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
+theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zbool.vo
+theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
+theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
+theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
+theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
+theories/Bool/DecBool.vo: theories/Bool/DecBool.v
+theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
+theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
+theories/Bool/Bool.vo: theories/Bool/Bool.v
+theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo
+theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
+theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
+theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
+theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable.vo
+theories/Arith/EqNat.vo: theories/Arith/EqNat.v
+theories/Arith/Even.vo: theories/Arith/Even.v
+theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo theories/Arith/Lt.vo
+theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
+theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
+theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
+theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Logic/Decidable.vo
+theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
+theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Le.vo: theories/Arith/Le.v
+theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Logic/JMeq.vo: theories/Logic/JMeq.v
+theories/Logic/Decidable.vo: theories/Logic/Decidable.v
+theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
+theories/Logic/Berardi.vo: theories/Logic/Berardi.v
+theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v
+theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/ProofIrrelevance.vo
+theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
+theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
+theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
+theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
+theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/Hurkens.vo
+theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v
+theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/PeanoSyntax.vo theories/Init/Wf.vo
+theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
+theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
+theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
+theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
+theories/Init/PeanoSyntax.vo: theories/Init/PeanoSyntax.v theories/Init/Datatypes.vo theories/Init/Peano.vo
+theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
+theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
+theories/Init/Datatypes.vo: theories/Init/Datatypes.v
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4e4b51833f..d8663f09d3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -311,8 +311,8 @@ let ident_or_meta_to_ct_ID = function
 let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
 let reference_to_ct_ID = function
-  | RIdent (_,id) -> CT_ident (Names.string_of_id id)
-  | RQualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
+  | Coqast.RIdent (_,id) -> CT_ident (Names.string_of_id id)
+  | Coqast.RQualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
 
 let xlate_class = function
   | FunClass -> CT_ident "FUNCLASS"
@@ -986,7 +986,7 @@ and (xlate_call_or_tacarg:raw_tactic_arg -> ct_TACTIC_COM) =
 	  (reference_to_ct_ID r,
 	    CT_tactic_arg_list(xlate_tacarg a,List.map xlate_tacarg l))
     | TacCall (_,_,_) -> xlate_error ""
-    | Reference (RIdent (_,s)) -> ident_tac s
+    | Reference (Coqast.RIdent (_,s)) -> ident_tac s
     | t -> xlate_error "TODO: result other than tactic or constr"
 
 and xlate_red_tactic =
@@ -1906,7 +1906,14 @@ let xlate_vernac =
          	| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg]) ->
          	        (syntaxop phy s spatarg unparg 
          coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*)
-   | VernacInfix (str_assoc, n, str, id) ->
+   | VernacOpenScope sc -> xlate_error "TODO: open scope"
+
+   | VernacDelimiters _ -> xlate_error "TODO: Delimiters"
+
+   | VernacNotation _ -> xlate_error "TODO: Notation"
+
+   | VernacInfix (str_assoc, n, str, id, sc) ->
+      (* TODO: handle scopes *)
       CT_infix (
        (match str_assoc with
         | Some Gramext.LeftA -> CT_lefta
@@ -1949,7 +1956,7 @@ let xlate_vernac =
      VernacSetOption (_, _)|VernacUnsetOption _|VernacDeclareImplicits (_, _)|
      VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
-     VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _)|
+     VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _, _)|
      VernacTacticGrammar _|VernacVar _|VernacTime _|VernacNop|VernacComments _)
     -> xlate_error "TODO: vernac"
 
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index f0ccfb886e..0df34f4223 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -1622,7 +1622,7 @@ Theorem exact_divide_valid :
 
 Unfold valid1 exact_divide; Intros k1 k2 t e p1; (Simplify ());Simpl; Auto;
 (Elim_eq_term  '(scalar_norm t (Tmult k2 (Tint k1))) 't1); Simpl; Auto;
-(Elim_eq_Z 'k1 'ZERO); Simpl; Auto;  Intros H1 H2; Elim H2; 
+(Elim_eq_Z 'k1 '(ZERO)); Simpl; Auto;  Intros H1 H2; Elim H2; 
 Elim scalar_norm_stable; Simpl; Generalize H1; Case (interp_term e k2);
 Try Trivial; (Case k1; Simpl; [
   Intros; Absurd `0 = 0`; Assumption
diff --git a/lib/bignat.ml b/lib/bignat.ml
new file mode 100644
index 0000000000..bb567cc241
--- /dev/null
+++ b/lib/bignat.ml
@@ -0,0 +1,99 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Arbitrary big natural numbers *)
+
+type bignat = int array
+
+let digits =            8
+let base =      100000000 (* let enough room for multiplication by 2 *)
+let base_div_2 = 50000000
+
+let of_string s =
+  let a = Array.create (String.length s / digits + 1) 0 in
+  let r = String.length s mod digits in
+  if r<>0 then a.(0) <- int_of_string (String.sub s 0 r);
+  for i = 1 to String.length s / digits do
+    a.(i) <- int_of_string (String.sub s ((i-1)*digits+r) digits)
+  done;
+  a
+
+let rec to_string s =
+  if s = [||] then "0" else
+    if s.(0) = 0 then to_string (Array.sub s 1 (Array.length s - 1))
+    else String.concat "" (Array.to_list (Array.map string_of_int s))
+  
+let is_nonzero a =
+  let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
+
+let one = [|1|]
+
+let is_one a =
+  let rec leading_zero i = i<0 || (a.(i) = 0 && leading_zero (i-1)) in
+  (a.(Array.length a - 1) = 1) && leading_zero (Array.length a - 2)
+      
+let div2_with_rest n =
+  let len = Array.length n in
+  let q = Array.create len 0 in
+  for i = 0 to len - 2 do
+    q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- base_div_2 * (n.(i) mod 2)
+  done;
+  q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
+  q, (n.(len - 1) mod 2) = 1
+
+let add_1 n =
+  let m = Array.copy n
+  and i = ref (Array.length n - 1) in
+  while !i >= 0 && m.(!i) = base-1 do
+    m.(!i) <- 0; decr i; 
+  done;
+  if !i < 0 then begin
+    m.(0) <- 0; Array.concat [[| 1 |]; m] 
+  end else begin
+    m.(!i) <- m.(!i) + 1; m
+  end
+
+let sub_1 n =
+  if is_nonzero n then
+    let m = Array.copy n
+    and i = ref (Array.length n - 1) in
+    while m.(!i) = 0 && !i > 0 do
+      m.(!i) <- base-1; decr i;
+    done;
+    m.(!i) <- m.(!i) - 1;
+    m
+  else n
+
+let rec mult_2 n =
+  let m = Array.copy n in
+  m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
+  for i = Array.length n - 2 downto 0 do
+    m.(i) <- 2 * m.(i);
+    if m.(i + 1) >= base then begin
+      m.(i + 1) <- m.(i + 1) - base; m.(i) <- m.(i) + 1 
+    end
+  done;
+  if m.(0) >= base then begin
+    m.(0) <- m.(0) - base; Array.concat [[| 1 |]; m] 
+  end else 
+    m
+
+let less_than m n =
+  let lm = ref 0 in
+  while !lm < Array.length m && m.(!lm) = 0 do incr lm done;
+  let ln = ref 0 in
+  while !ln < Array.length n && n.(!ln) = 0 do incr ln done;
+  let um = Array.length m - !lm and un = Array.length n - !ln in
+  let rec lt d =
+    d < um && (m.(!lm+d) < n.(!ln+d) || (m.(!lm+d) = n.(!ln+d) && lt (d+1)))
+  in
+  (um < un) || (um = un && lt 0)
+
+type bigint = POS of bignat | NEG of bignat
diff --git a/lib/bignat.mli b/lib/bignat.mli
new file mode 100644
index 0000000000..173d43e4ca
--- /dev/null
+++ b/lib/bignat.mli
@@ -0,0 +1,29 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Arbitrary big natural numbers *)
+
+type bignat
+
+val of_string : string -> bignat
+val to_string : bignat -> string
+
+val is_nonzero : bignat -> bool
+val one : bignat
+val is_one : bignat -> bool
+val div2_with_rest : bignat -> bignat * bool (* true=odd; false=even *)
+
+val add_1 : bignat -> bignat
+val sub_1 : bignat -> bignat (* Remark: (sub_1 0)=0 *)
+val mult_2 : bignat -> bignat
+
+val less_than : bignat -> bignat -> bool
+
+type bigint = POS of bignat | NEG of bignat
diff --git a/parsing/ast.ml b/parsing/ast.ml
index a41e627e6e..52a390af1f 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Libnames
 open Coqast
-open Tacexpr
 open Genarg
 
 let isMeta s = String.length s <> 0 & s.[0]='$'
@@ -239,7 +238,9 @@ let coerce_reference_to_id = function
 
 let slam_ast (_,fin) id ast =
   match id with
-    | Coqast.Nvar ((deb,_), s) -> Coqast.Slam ((deb,fin), Some s, ast)
+    | Coqast.Nvar ((deb,_), s) -> 
+	let name = if s = id_of_string "_" then None else Some s in
+	Coqast.Slam ((deb,fin), name, ast)
     | Coqast.Nmeta ((deb,_), s) -> Coqast.Smetalam ((deb,fin), s, ast)
     | _ -> invalid_arg "Ast.slam_ast"
 
@@ -269,7 +270,7 @@ let env_assoc_value loc v env =
   with Not_found -> 
     anomaly_loc
       (loc,"Ast.env_assoc_value",
-       (str"metavariable " ++ str v ++ str" is unbound."))
+       (str"metavariable " ++ str v ++ str" is unbound"))
 
 let env_assoc_list sigma (loc,v) =
   match env_assoc_value loc v sigma with
@@ -404,7 +405,7 @@ let typed_ast_match env p a = match (p,a) with
 
 let astl_match = amatchl []
 
-let ast_first_match pat_of_fun env ast sl =
+let first_match pat_of_fun env ast sl =
   let rec aux = function
     | [] -> None
     | h::t ->
@@ -413,12 +414,13 @@ let ast_first_match pat_of_fun env ast sl =
   in 
   aux sl
 
-let first_match pat_of_fun env ast sl =
+let find_all_matches pat_of_fun env ast sl =
   let rec aux = function
-    | [] -> None
+    | [] -> []
     | (h::t) ->
-        (try Some (h, ast_match env (pat_of_fun h) ast)
-         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
+        let l = aux t in
+        (try (h, ast_match env (pat_of_fun h) ast)::l
+         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> l)
   in 
   aux sl
 
@@ -695,7 +697,7 @@ let rec eval_act dloc sigma = function
   | ActCase(e,ml) ->
       (match eval_act dloc sigma e with
         | (PureAstNode esub) ->
-            (match ast_first_match myfst sigma esub ml with
+            (match first_match myfst sigma esub ml with
               | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a
               | _ -> case_failed dloc sigma esub (List.map myfst ml))
         | _ -> grammar_type_error (dloc,"Ast.eval_act"))
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 07dbd06f29..9fd8e9cc92 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -103,7 +103,7 @@ val coerce_to_id : Coqast.t -> identifier
 
 val coerce_qualid_to_id : qualid Util.located -> identifier
 
-val coerce_reference_to_id : Tacexpr.reference_expr -> identifier
+val coerce_reference_to_id : reference_expr -> identifier
 
 val abstract_binders_ast :
   Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t
@@ -144,7 +144,7 @@ val replace_vars_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
 val bind_env : env -> string -> typed_ast -> env
 val ast_match : env -> astpat -> Coqast.t -> env
 val astl_match : env -> patlist -> Coqast.t list -> env
-val first_match : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) option
+val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
 val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
   ('a * env) option
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 89025de4f4..03e652ccea 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -196,7 +196,7 @@ let maybe_constructor allow_var env = function
       let qid = interp_qualid l in
       (try match extended_locate qid with
        | SyntacticDef sp ->
-	   (match Syntax_def.search_syntactic_definition sp with
+	   (match Syntax_def.search_syntactic_definition loc sp with
 	    | RRef (_,(ConstructRef c as x)) ->
 		if !dump then add_glob loc x; 
  		ConstrPat (loc,c)
@@ -267,7 +267,7 @@ let ast_to_global loc c =
     | ("EVAR", [(Num (_,ev))]) ->
 	REvar (loc, ev), []
     | ("SYNCONST", [sp]) ->
-	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
+	Syntax_def.search_syntactic_definition loc (ast_to_sp sp), []
     | _ -> anomaly_loc (loc,"ast_to_global",
 			(str "Bad ast for this global a reference"))
 
@@ -285,7 +285,7 @@ let ref_from_constr c = match kind_of_term c with
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let ast_to_var (env,impls) (vars1,vars2) loc id =
+let ast_to_var (env,impls,_) (vars1,vars2) loc id =
   let imps =
     if Idset.mem id env or List.mem id vars1
     then
@@ -322,7 +322,7 @@ let rawconstr_of_qualid env vars loc qid =
     let imps = implicits_of_global ref in
     RRef (loc, ref), imps
   | SyntacticDef sp ->
-    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp), []
+    Syntax_def.search_syntactic_definition loc sp, []
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -352,7 +352,7 @@ let message_redundant_alias (s1,s2) =
   warning ("Alias variable "^(string_of_id s1)
 	   ^" is merged with "^(string_of_id s2))
 
-let rec ast_to_pattern env aliases = function
+let rec ast_to_pattern (_,_,scopes as env) aliases = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
       let aliases' = merge_aliases aliases (name_of_nvar s) in
       ast_to_pattern env aliases' p
@@ -369,6 +369,16 @@ let rec ast_to_pattern env aliases = function
 	     user_err_loc (loc,"ast_to_pattern",mssg_hd_is_not_constructor s)
 *)
               assert false)
+  | Node(_,"PATTNUMERAL", [Str(loc,n)]) ->
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.POS (Bignat.of_string n))
+	(alias_of aliases) scopes)
+
+  | Node(_,"PATTNEGNUMERAL", [Str(loc,n)]) ->
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.NEG (Bignat.of_string n))
+	(alias_of aliases) scopes)
+
   | ast ->
       (match maybe_constructor true env ast with
 	 | ConstrPat (loc,c) -> ([aliases], PatCstr (loc,c,[],alias_of aliases))
@@ -420,8 +430,17 @@ let set_hole_implicit i = function
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
   | _ -> anomaly "Only refs have implicits"
 
+let build_expression loc1 loc2 (ref,impls) args =
+  let rec add_args n = function
+    | true::impls,args -> (RHole (set_hole_implicit n (RRef (loc2,ref))))::add_args (n+1) (impls,args)
+    | false::impls,a::args -> a::add_args (n+1) (impls,args)
+    | [], args -> args
+    | _ -> anomalylabstrm "astterm"
+      (str "Incorrect signature " ++ pr_global_env None ref ++ str " as an infix") in
+  RApp (loc1,RRef (loc2,ref),add_args 1 (impls,args))
+
 let ast_to_rawconstr sigma env allow_soapp lvar =
-  let rec dbrec (ids,impls as env) = function
+  let rec dbrec (ids,impls,scopes as env) = function
     | Nvar(loc,s) ->
 	fst (rawconstr_of_var env lvar loc s)
 
@@ -436,7 +455,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
           with Not_found ->
 	    error_fixname_unbound "ast_to_rawconstr (FIX)" false locid iddef in
 	let ext_ids = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (dbrec (ext_ids,impls)) lt) in
+	let defl = Array.of_list (List.map (dbrec (ext_ids,impls,scopes)) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
 	  
@@ -449,7 +468,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	    error_fixname_unbound "ast_to_rawconstr (COFIX)" true locid iddef
 	in
 	let ext_ids = List.fold_right Idset.add lf ids in
-	let defl = Array.of_list (List.map (dbrec (ext_ids,impls)) lt) in
+	let defl = Array.of_list (List.map (dbrec (ext_ids,impls,scopes)) lt) in
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
 	  
@@ -457,7 +476,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let na,ids' = match ona with
 	  | Some id -> Name id, Idset.add id ids
 	  | _ -> Anonymous, ids in
-	let c1' = dbrec env c1 and c2' = dbrec (ids',impls) c2 in
+	let c1' = dbrec env c1 and c2' = dbrec (ids',impls,scopes) c2 in
 	(match k with
 	   | "PROD" -> RProd (loc, na, c1', c2')
 	   | "LAMBDA" -> RLambda (loc, na, locate_if_isevar locna na c1', c2')
@@ -467,6 +486,20 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
     | Node(_,("PRODLIST"|"LAMBDALIST" as s), [c1;(Slam _ as c2)]) -> 
 	iterated_binder s 0 c1 env c2
 
+    | Node(loc1,"NOTATION", Str(loc2,ntn)::args) ->
+	Symbols.interp_notation ntn scopes (List.map (dbrec env) args)
+
+    | Node(_,"NUMERAL", [Str(loc,n)]) ->
+	Symbols.interp_numeral loc (Bignat.POS (Bignat.of_string n))
+	  scopes
+
+    | Node(_,"NEGNUMERAL", [Str(loc,n)]) ->
+	Symbols.interp_numeral loc (Bignat.NEG (Bignat.of_string n))
+	  scopes
+
+    | Node(_,"DELIMITERS", [Str(_,sc);e]) ->
+	dbrec (ids,impls,sc::scopes) e
+
     | Node(loc,"APPLISTEXPL", f::args) ->
 	RApp (loc,dbrec env f,ast_to_args env args)
 
@@ -536,7 +569,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 
     | _ -> anomaly "ast_to_rawconstr: unexpected ast"
 
-  and ast_to_eqn n (ids,impls as env) = function
+  and ast_to_eqn n (ids,impls,scopes as env) = function
     | Node(loc,"EQN",rhs::lhs) ->
 	let (idsl_substl_list,pl) =
 	  List.split (List.map (ast_to_pattern env ([],[])) lhs) in
@@ -550,10 +583,10 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let rhs = replace_vars_ast subst rhs in
 	List.iter message_redundant_alias subst;
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
-	(loc, eqn_ids,pl,dbrec (env_ids,impls) rhs)
+	(loc, eqn_ids,pl,dbrec (env_ids,impls,scopes) rhs)
     | _ -> anomaly "ast_to_rawconstr: ill-formed ast for Cases equation"
 
-  and iterated_binder oper n ty (ids,impls as env) = function
+  and iterated_binder oper n ty (ids,impls,scopes as env) = function
     | Slam(loc,ona,body) ->
 	let na,ids' = match ona with 
 	  | Some id ->
@@ -561,7 +594,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	      Name id, Idset.add id ids
 	  | _ -> Anonymous, ids
 	in
-	let r = iterated_binder oper (n+1) ty (ids',impls) body in
+	let r = iterated_binder oper (n+1) ty (ids',impls,scopes) body in
 	(match oper with
 	   | "PRODLIST" -> RProd(loc, na, dbrec env ty, r)
 	   | "LAMBDALIST" ->
@@ -715,7 +748,7 @@ let globalize_ast ast =
 
 let interp_rawconstr_gen sigma env impls allow_soapp lvar com =
   ast_to_rawconstr sigma
-    (from_list (ids_of_rel_context (rel_context env)), impls)
+    (from_list (ids_of_rel_context (rel_context env)), impls, Symbols.current_scopes ())
     allow_soapp (lvar,env) com
 
 let interp_rawconstr sigma env com =
@@ -748,7 +781,7 @@ let constrOut = function
       (str "Not a Dynamic ast: " ++ print_ast ast)
 
 let interp_global_constr env (loc,qid) = 
-  let c,_ = rawconstr_of_qualid (Idset.empty,[]) ([],env) loc qid in
+  let c,_ = rawconstr_of_qualid (Idset.empty,[],Symbols.current_scopes()) ([],env) loc qid in
   understand Evd.empty env c
 
 let interp_constr sigma env c =
@@ -869,7 +902,7 @@ let pattern_of_rawconstr lvar c =
 let interp_constrpattern_gen sigma env lvar com = 
   let c =
     ast_to_rawconstr sigma
-      (from_list (ids_of_rel_context (rel_context env)), [])
+      (from_list (ids_of_rel_context (rel_context env)), [], Symbols.current_scopes ())
       true (List.map fst lvar,env) com
   and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   try 
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 96743098cf..5c0fef4aa9 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -34,8 +34,10 @@ let nat_path = make_path datatypes_module (id_of_string "nat")
 
 let glob_nat = IndRef (nat_path,0)
 
-let glob_O = ConstructRef ((nat_path,0),1)
-let glob_S = ConstructRef ((nat_path,0),2)
+let path_of_O = ((nat_path,0),1)
+let path_of_S = ((nat_path,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
 
 let eq_path = make_path logic_module (id_of_string "eq")
 let eqT_path = make_path logic_type_module (id_of_string "eqT")
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
index 8eedab0500..dbe99e3991 100644
--- a/parsing/coqlib.mli
+++ b/parsing/coqlib.mli
@@ -27,6 +27,8 @@ val logic_type_module : dir_path
 
 (* Natural numbers *)
 val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
 val glob_O : global_reference
 val glob_S : global_reference
 
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index b3d0278028..9f802563b8 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -18,6 +18,7 @@ open Extend
 open Vernacexpr
 open Names
 open Nametab
+open Symbols
 
 (*** Syntax keys ***)
 
@@ -114,7 +115,7 @@ let find_syntax_entry whatfor gt =
     List.flatten
       (List.map (fun k -> Gmapl.find (whatfor,k) !from_key_table) gt_keys)
   in 
-  first_match (fun se -> se.syn_astpat) [] gt entries
+  find_all_matches (fun se -> se.syn_astpat) [] gt entries
 
 let remove_with_warning name =
   if Gmap.mem name !from_name_table then begin
@@ -139,10 +140,9 @@ let add_ppobject {sc_univ=wf;sc_entries=sel} = List.iter (add_rule wf) sel
 
 (* Pretty-printing machinery *)
 
-type std_printer = Coqast.t -> std_ppcmds
+type std_printer = Genarg.constr_ast -> std_ppcmds
 type unparsing_subfunction = string -> tolerability option -> std_printer
-
-type std_constr_printer = Genarg.constr_ast -> std_ppcmds
+type primitive_printer = Genarg.constr_ast -> std_ppcmds option
 
 (* Module of primitive printers *)
 module Ppprim =
@@ -153,94 +153,111 @@ module Ppprim =
     let add (a,ppr) = tab := (a,ppr)::!tab
   end
 
-(* A printer for the tokens. *)
-let token_printer stdpr = function
-  | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast
-  | a -> stdpr a
+(**********************************************************************)
+(* Primitive printers (e.g. for numerals)                             *)
+
+(* This is the map associating to a printer the scope it belongs to   *)
+(* and its ML code                                                    *)
+
+let primitive_printer_tab = 
+  ref (Stringmap.empty : (scope_name * primitive_printer) Stringmap.t)
+let declare_primitive_printer s sc pp =
+  primitive_printer_tab := Stringmap.add s (sc,pp) !primitive_printer_tab
+let lookup_primitive_printer s =
+  Stringmap.find s !primitive_printer_tab
 
 (* Register the primitive printer for "token". It is not used in syntax/PP*.v,
  * but any ast matching no PP rule is printed with it. *)
+(*
+let _ = declare_primitive_printer "token" token_printer
+*)
 
-let _ = Ppprim.add ("token",token_printer)
+(* A printer for the tokens. *)
+let token_printer stdpr = function
+  | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast
+  | a -> stdpr a
 
 (* A primitive printer to do "print as" (to specify a length for a string) *)
-let print_as_printer stdpr = function
-  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> stras (n,s)
-  | ast                                  -> stdpr ast
+let print_as_printer = function
+  | Node (_, "AS", [Num(_,n); Str(_,s)]) -> Some (stras (n,s))
+  | ast                                  -> None
 
-let _ = Ppprim.add ("print_as",print_as_printer)
+let _ = declare_primitive_printer "print_as" default_scope print_as_printer
 
 (* Handle infix symbols *)
 
-let find_infix_symbols sp =
-  try Spmap.find sp !infix_names_map with Not_found -> []
-
-let find_infix_name a =
-  try Stringmap.find a !infix_symbols_map
-  with Not_found -> anomaly ("Undeclared symbol: "^a)
-
-let declare_infix_symbol sp s =
-  let l = find_infix_symbols sp in
-  infix_names_map := Spmap.add sp (s::l) !infix_names_map;
-  infix_symbols_map := Stringmap.add s sp !infix_symbols_map
-
-let meta_pattern m = Pmeta(m,Tany)
-
-let make_hunks (lp,rp) s e1 e2 =
-  let n,s =
-    if is_letter (s.[String.length s -1]) or is_letter (s.[0])
-    then 1,s^" " else 0,s
-  in
-  [PH (meta_pattern e1, None, lp);
-   UNP_BRK (n, 1); RO s;
-   PH (meta_pattern e2, None, rp)]
-
-let build_syntax (ref,e1,e2,assoc) =
-  let sp = match ref with
-  | TrueGlobal r -> Nametab.sp_of_global None r
-  | SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in
-  let rec find_symbol = function
-    | [] ->
-	let s = match ref with
-	  | TrueGlobal r ->
-	      string_of_qualid (shortest_qualid_of_global None r)
-	  | SyntacticDef _ -> string_of_path sp in
-	UNP_BOX (PpHOVB 0,
-	  [RO "("; RO s; UNP_BRK (1, 1); PH (meta_pattern e1, None, E);
-	   UNP_BRK (1, 1); PH (meta_pattern e2, None, E); RO ")"])
-    | a::l ->
-	if find_infix_name a = sp then
-	  UNP_BOX (PpHOVB 1, make_hunks assoc a e1 e2)
-	else
-	  find_symbol l
-  in find_symbol (find_infix_symbols sp)
-
+let pr_parenthesis inherited se strm =
+  let rule_prec = (se.syn_id, se.syn_prec) in
+  let no_paren = tolerable_prec inherited rule_prec in
+  if no_paren then 
+    strm
+  else 
+    (str"(" ++ strm ++ str")")
+    
+let print_delimiters inh se strm = function
+  | None -> pr_parenthesis inh se strm
+  | 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
 
 (* Print the syntax entry. In the unparsing hunks, the tokens are
  * printed using the token_printer, unless another primitive printer
  * is specified. *)
 
-let print_syntax_entry whatfor sub_pr env se = 
-  let rule_prec = (se.syn_id, se.syn_prec) in
-  let rec print_hunk = function
+let print_syntax_entry sub_pr scopes env se = 
+  let rec print_hunk rule_prec scopes = function
     | PH(e,externpr,reln) ->
 	let node = Ast.pat_sub Ast.dummy_loc env e in
 	let printer =
 	  match externpr with (* May branch to an other printer *)
 	    | Some c ->
                 (try (* Test for a primitive printer *) Ppprim.map c
-                with Not_found -> token_printer )
+                with Not_found -> token_printer)
 	    | _ -> token_printer in
-	printer (sub_pr whatfor (Some(rule_prec,reln))) node
+	printer (sub_pr scopes (Some(rule_prec,reln))) node
     | RO s -> str s
     | UNP_TAB -> tab ()
     | UNP_FNL -> fnl ()
     | UNP_BRK(n1,n2) -> brk(n1,n2)
     | UNP_TBRK(n1,n2) -> tbrk(n1,n2)
-    | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist print_hunk sub)
-    | UNP_INFIX (sp,e1,e2,assoc) -> print_hunk (build_syntax (sp,e1,e2,assoc))
+    | UNP_BOX (b,sub) -> ppcmd_of_box b (prlist (print_hunk rule_prec scopes) sub)
+    | UNP_SYMBOLIC _ -> anomaly "handled by call_primitive_parser"
   in 
-  prlist print_hunk se.syn_hunks
+  let rule_prec = (se.syn_id, se.syn_prec) in
+  prlist (print_hunk rule_prec scopes) se.syn_hunks
+
+let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
+  try (
+  match se.syn_hunks with
+    | [PH(e,Some c,reln)] ->
+	  (* 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
+	    | None -> otherwise ()
+	    | Some (dlm,scopes) ->
+	        (* We can use this printer *)
+	        let node = Ast.pat_sub Ast.dummy_loc env e in
+	        match pr node with
+		  | Some strm -> print_delimiters inherited se strm dlm
+		  | None -> otherwise ())
+    | [UNP_SYMBOLIC (sc,pat,sub)] ->
+	(match Symbols.find_notation sc pat scopes with
+	  | None -> otherwise ()
+	  | Some (dlm,scopes) ->
+	      print_delimiters inherited se
+		(print_syntax_entry rec_pr scopes env 
+		  {se with syn_hunks = [sub]}) dlm)
+    | _ ->
+	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
+  )
+  with Not_found -> (* To handle old style printer *)
+	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
 
 (* [genprint whatfor dflt inhprec ast] prints out the ast of
  * 'universe' whatfor. If the term is not matched by any
@@ -250,20 +267,19 @@ let print_syntax_entry whatfor sub_pr env se =
  * global constants basenames. *)
 
 let genprint dflt whatfor inhprec ast =
-  let rec rec_pr whatfor inherited gt =
-    match find_syntax_entry whatfor gt with
-      | Some(se, env) ->     
-	  let rule_prec = (se.syn_id, se.syn_prec) in
-	  let no_paren = tolerable_prec inherited rule_prec in
-	  let printed_gt = print_syntax_entry whatfor rec_pr env se in
-	  if no_paren then 
-	    printed_gt
-	  else 
-	    (str"(" ++ printed_gt ++ str")")
-      | None -> dflt gt (* No rule found *)
+  let rec rec_pr scopes inherited gt =
+    let entries = find_syntax_entry whatfor gt in
+    let rec test_rule = function
+      | se_env::rules ->
+	  call_primitive_parser
+	    rec_pr 
+	    (fun () -> test_rule rules) 
+	    inherited scopes se_env
+      | [] -> dflt gt (* No rule found *)
+    in test_rule entries
   in
   try 
-    rec_pr whatfor inhprec ast
+    rec_pr (Symbols.current_scopes ()) inhprec ast
   with
     | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">")
     | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">")
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index 8e3445ed76..cf1b0de3f7 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -12,6 +12,7 @@
 open Pp
 open Extend
 open Vernacexpr
+open Symbols
 (*i*)
 
 (* Syntax entry tables. *)
@@ -25,27 +26,37 @@ val unfreeze : frozen_t -> unit
 
 (* Search and add a PP rule for an ast in the summary *)
 val find_syntax_entry :
-  string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) option
+  string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) list
 val add_rule : string -> Ast.astpat syntax_entry -> unit
 val add_ppobject : Ast.astpat syntax_command -> unit
 val warning_verbose : bool ref
 
 (* Pretty-printing *)
 
-type std_printer = Coqast.t -> std_ppcmds
+type std_printer = Genarg.constr_ast -> std_ppcmds
 type unparsing_subfunction = string -> tolerability option -> std_printer
+type primitive_printer = Genarg.constr_ast -> std_ppcmds option
 
-(* Module of constr primitive printers *)
+(* Module of constr primitive printers [old style - no scope] *)
 module Ppprim :
   sig
     type t = std_printer -> std_printer
     val add : string * t -> unit
   end
 
+val declare_primitive_printer : 
+  string -> scope_name -> primitive_printer -> unit
+
+(*
 val declare_infix_symbol : Libnames.section_path -> string -> unit
+*)
 
 (* Generic printing functions *) 
+(*
 val token_printer: std_printer -> std_printer
+*)
+(*
 val print_syntax_entry : 
   string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds
+*)
 val genprint : std_printer -> unparsing_subfunction
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 7c4c400ebb..a469a648f8 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -187,8 +187,7 @@ type 'pat unparsing_hunk =
   | UNP_TBRK of int * int
   | UNP_TAB
   | UNP_FNL
-  | UNP_INFIX of Libnames.extended_global_reference * string * string *
-      (parenRelation * parenRelation)
+  | UNP_SYMBOLIC of string * string * 'pat unparsing_hunk
 
 let rec subst_hunk subst_pat subst hunk = match hunk with
   | PH (pat,so,pr) ->
@@ -204,10 +203,10 @@ let rec subst_hunk subst_pat subst hunk = match hunk with
   | UNP_TBRK _
   | UNP_TAB
   | UNP_FNL -> hunk
-  | UNP_INFIX (ref,s1,s2,prs) ->
-      let ref' = Libnames.subst_ext subst ref in
-	if ref' == ref then hunk else
-	  UNP_INFIX (ref',s1,s2,prs)
+  | UNP_SYMBOLIC (s1, s2, pat) ->
+      let pat' = subst_hunk subst_pat subst pat in
+	if pat' == pat then hunk else
+	  UNP_SYMBOLIC (s1, s2, pat')
 
 (* Checks if the precedence of the parent printer (None means the
    highest precedence), and the child's one, follow the given
@@ -271,8 +270,8 @@ type syntax_entry_ast = precedence * syntax_rule list
 let rec interp_unparsing env = function
   | PH (ast,ext,pr) -> PH (Ast.val_of_ast env ast,ext,pr)
   | UNP_BOX (b,ul) -> UNP_BOX (b,List.map (interp_unparsing env) ul)
-  | UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL
-  | UNP_INFIX _ as x -> x
+  | UNP_BRK _ | RO _ | UNP_TBRK _ | UNP_TAB | UNP_FNL as x -> x
+  | UNP_SYMBOLIC (x,y,u) -> UNP_SYMBOLIC (x,y,interp_unparsing env u)
 
 let rule_of_ast univ prec (s,spat,unp) =
   let (astpat,meta_env) = Ast.to_pat [] spat in
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 8734e34525..7294a2bb0d 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -82,8 +82,11 @@ type 'pat unparsing_hunk =
   | UNP_TBRK of int * int
   | 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) -> 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index ede831944e..bac4892179 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -94,10 +94,10 @@ GEXTEND Gram
 	  VernacSearch (SearchRewrite c, l)
 
       (* TODO: rapprocher Eval et Check *)
-      | IDENT "Eval"; g = OPT natural; r = Tactic.red_expr; "in";
-	  c = constr -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Check"; g = OPT natural; c = constr ->
-	  VernacCheckMayEval (None, g, c)
+      | IDENT "Eval"; r = Tactic.red_expr; "in";
+	  c = constr -> VernacCheckMayEval (Some r, None, c)
+      | IDENT "Check"; c = constr ->
+	  VernacCheckMayEval (None, None, c)
       | "Type"; c = constr -> VernacGlobalCheck c      (* pas dans le RefMan *)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
@@ -218,10 +218,18 @@ GEXTEND Gram
      | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
+     | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
+
+     | IDENT "Delimiters"; left = STRING; sc = IDENT; right = STRING ->
+	 VernacDelimiters (sc,(left,right))
+
      (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
-     | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = qualid
-        -> VernacInfix (a,n,op,p)
-     | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid        -> VernacDistfix (a,n,s,p)
+     | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = qualid;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc)
+     | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
+     | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr;
+	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (a,n,s,c,sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 1ba2c6f233..6bee39b122 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -18,7 +18,12 @@ GEXTEND Gram
 
   pattern:
     [ [ qid = global -> qid
-      | "("; p = compound_pattern; ")" -> p ] ]
+      | "("; p = compound_pattern; ")" -> p
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (PATTNUMERAL $n) >>
+      | "-"; n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (PATTNEGNUMERAL $n) >>
+    ] ]
   ;
   compound_pattern:
     [ [ p = pattern ; lp = ne_pattern_list ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index cbe3a14c24..4f8cbaa8c7 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,7 +17,7 @@ GEXTEND Gram
   GLOBAL: constr0 constr1 constr2 constr3 lassoc_constr4 constr5
           constr6 constr7 constr8 constr9 constr10 lconstr constr
           ne_ident_comma_list ne_constr_list sort ne_binders_list qualid
-          global constr_pattern ident;
+          global constr_pattern ident numarg;
   ident:
     [ [ id = Prim.var -> id
 
@@ -94,6 +94,10 @@ GEXTEND Gram
           <:ast< (COFIX $id ($LIST $fbinders)) >>
       | s = sort -> s
       | v = global -> v
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
+      | "-"; n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NEGNUMERAL $n) >>
   ] ]
   ;
   constr1:
@@ -169,9 +173,12 @@ GEXTEND Gram
     [ [ c1 = constr8 -> c1
       | c1 = constr8; "::"; c2 = constr8 -> <:ast< (CAST $c1 $c2) >> ] ]
   ;
+  numarg:
+    [ [ n = Prim.natural -> Coqast.Num (loc, n) ] ]
+  ;
   simple_binding:
     [ [ id = ident; ":="; c = constr -> <:ast< (BINDING $id $c) >>
-      | n = Prim.numarg; ":="; c = constr -> <:ast< (BINDING $n $c) >> ] ]
+      | n = numarg; ":="; c = constr -> <:ast< (BINDING $n $c) >> ] ]
   ;
   simple_binding_list:
     [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
@@ -181,7 +188,7 @@ GEXTEND Gram
           Coqast.Node
             (loc, "EXPLICITBINDINGS",
              (Coqast.Node (loc, "BINDING", [Ast.coerce_to_var c1; c2]) :: bl))
-      | n = Prim.numarg; ":="; c = constr; bl = simple_binding_list ->
+      | n = numarg; ":="; c = constr; bl = simple_binding_list ->
           <:ast<(EXPLICITBINDINGS (BINDING $n $c) ($LIST $bl))>>
       | c1 = constr; bl = LIST0 constr ->
           <:ast<(IMPLICITBINDINGS $c1 ($LIST $bl))>> ] ]
@@ -234,9 +241,10 @@ GEXTEND Gram
       | -> <:ast< (ISEVAR) >> ] ]
   ;
   constr91:
-    [ [ n = Prim.natural; "!"; c1 = constr9 ->
-      let n = Coqast.Num (loc,n) in
-          <:ast< (EXPL $n $c1) >>
+    [ [ n = INT; "!"; c1 = constr9 ->
+          let n = Coqast.Num (loc,int_of_string n) in <:ast< (EXPL $n $c1) >>
+      | n = INT ->
+	  let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
       | c1 = constr9 -> c1 ] ]
   ;
   ne_constr91_list:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index fe6561b972..859865ee45 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -13,15 +13,17 @@
 open Pp
 open Util
 open Ast
-open Pcoq
 open Coqast
 open Rawterm
 open Tacexpr
 open Ast
-open Tactic
 
 ifdef Quotify then
 open Qast
+else
+open Pcoq
+
+open Tactic
 
 ifdef Quotify then
 open Q
@@ -31,26 +33,32 @@ type let_clause_kind =
   | LETCLAUSE of
       (Names.identifier Util.located * Genarg.constr_ast may_eval option * raw_tactic_arg)
 
-let fail_default_value = 0
-
-let out_letin_clause loc = function
-  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
-  | LETCLAUSE (id,c,d) -> (id,c,d)
-
-let make_letin_clause _ = List.map (out_letin_clause dummy_loc)
-
 ifdef Quotify then
+module Prelude = struct
 let fail_default_value = Qast.Int "0"
 
-ifdef Quotify then
 let out_letin_clause loc = function
   | Qast.Node ("LETTOPCLAUSE", _) -> user_err_loc (loc, "", (str "Syntax Error"))
   | Qast.Node ("LETCLAUSE", [id;c;d]) ->
       Qast.Tuple [id;c;d]
+  | _ -> anomaly "out_letin_clause"
 
-ifdef Quotify then
-let make_letin_clause loc = function
-  | Qast.List l -> Qast.List (List.map (out_letin_clause loc) l)
+let make_letin_clause _ = function
+  | Qast.List l -> Qast.List (List.map (out_letin_clause dummy_loc) l)
+  | _ -> anomaly "make_letin_clause"
+end
+else
+module Prelude = struct
+let fail_default_value = 0
+
+let out_letin_clause loc = function
+  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
+  | LETCLAUSE (id,c,d) -> (id,c,d)
+
+let make_letin_clause loc = List.map (out_letin_clause loc)
+end
+
+open Prelude
 
 (* Tactics grammar rules *)
 
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 97ffba1d0d..ae36762326 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -21,8 +21,6 @@ open Coqlib
 open Termast
 open Extend
 
-exception Non_closed_number
-
 let ast_O = ast_of_ref glob_O
 let ast_S = ast_of_ref glob_S
   
@@ -55,6 +53,8 @@ let nat_of_string s dloc =
 let pat_nat_of_string s dloc = 
   pat_nat_of_int (int_of_string s) dloc
     
+exception Non_closed_number
+
 let rec int_of_nat_rec astS astO p =
   match p with
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) ->
@@ -84,6 +84,8 @@ let nat_printer std_pr p =
     | Some i -> str (string_of_int i)
     | None -> pr_S (pr_external_S std_pr p)
 
+let nat_printer_0 _ _ = str "0"
+
 let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
 
 (* Declare the primitive parser *)
@@ -104,3 +106,79 @@ let _ =
     [None, None,
      [[Gramext.Stoken ("INT", "")],
       Gramext.action pat_nat_of_string]]
+
+
+(**********************************************************************)
+(* Parsing *)
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+
+open Rawterm
+open Libnames
+open Bignat
+open Symbols
+
+let nat_of_int dloc = function
+  | POS n ->
+      if less_than (of_string "5000") n & Options.is_verbose () then begin
+	warning ("You may experiment stack overflow and segmentation fault\
+                  \nwhile parsing numbers in nat greater than 5000");
+	flush_all ()
+      end;
+      let ref_O = RRef (dloc, glob_O) in
+      let ref_S = RRef (dloc, glob_S) in
+      let rec mk_nat n =
+	if is_nonzero n then 
+	  RApp (dloc,ref_S, [mk_nat (sub_1 n)])
+	else 
+	  ref_O
+      in 
+      mk_nat n
+  | NEG n ->
+      user_err_loc (dloc, "nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+
+let pat_nat_of_int dloc n name = match n with
+  | POS n -> 
+      let rec mk_nat n name =
+	if is_nonzero n then 
+	  PatCstr (dloc,path_of_S,[mk_nat (sub_1 n) Anonymous],name)
+	else 
+	  PatCstr (dloc,path_of_O,[],name)
+      in 
+      mk_nat n name
+  | NEG n ->
+      user_err_loc (dloc, "pat_nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+let _ = 
+  Symbols.declare_numeral_interpreter "nat_scope"
+    (nat_of_int,Some pat_nat_of_int)
+
+(***********************************************************************)
+(* Printing *)
+
+exception Non_closed_number
+
+let rec int_of_nat = function
+  | Node (_,"APPLIST", [b; a]) when alpha_eq(b,ast_S) -> (int_of_nat a) + 1
+  | a when alpha_eq(a,ast_O) -> 0
+  | _ -> raise Non_closed_number
+	  
+(* Prints not p, but the SUCCESSOR of p !!!!! *)
+let nat_printer_S p =
+  try 
+    Some (int (int_of_nat p + 1))
+  with
+    Non_closed_number -> None
+
+let nat_printer_O _ =
+  Some (int 0)
+
+(* Declare the primitive printers *)
+let _ =
+  Esyntax.declare_primitive_printer "nat_printer_S" "nat_scope" nat_printer_S
+
+let _ = 
+  Esyntax.declare_primitive_printer "nat_printer_O" "nat_scope" nat_printer_O
+
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d279499ab4..5363be6334 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -73,7 +73,7 @@ open Q
 
 GEXTEND Gram
   GLOBAL: var ident natural metaident integer string preident ast astpat
-  astact astlist qualid reference dirpath rawident numarg;
+  astact astlist qualid reference dirpath rawident;
 
   metaident:
     [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
@@ -97,9 +97,6 @@ GEXTEND Gram
     [ [ i = INT      -> local_make_posint i
       | "-"; i = INT -> local_make_negint i ] ]
   ;
-  numarg:
-    [ [ i = INT -> Num(loc, int_of_string i) ] ]
-  ;
   field:
     [ [ s = FIELD -> local_id_of_string s ] ]
   ;
@@ -121,8 +118,8 @@ GEXTEND Gram
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Tacexpr.RQualid (loc, local_make_qualid (local_append l id) id')
-      | id = ident -> Tacexpr.RIdent (loc,id)
+        Coqast.RQualid (loc, local_make_qualid (local_append l id) id')
+      | id = ident -> Coqast.RIdent (loc,id)
       ] ]
   ;
   string:
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index bc2fb999f9..6c58296274 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -14,8 +14,6 @@ open Names
 open Pcoq
 open Extend
 
-exception Non_closed_number
-
 let get_r_sign loc =
   let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
   ((ast_of_id (id_of_string "R0"),
@@ -23,6 +21,7 @@ let get_r_sign loc =
     ast_of_id (id_of_string "Rplus"), 
     ast_of_id (id_of_string "NRplus")))
 
+(* Parsing via Grammar *)
 let r_of_int n dloc =
   let (ast0,ast1,astp,_) = get_r_sign dloc in
   let rec mk_r n =
@@ -48,14 +47,16 @@ let _ =
 
 (** pp **)
 
+exception Non_closed_number
+
 let rec int_of_r_rec ast1 astp p =
   match p with
     | Node (_,"APPLIST", [b; a; c]) when alpha_eq(b,astp) && 
                                          alpha_eq(a,ast1) ->
-	(int_of_r_rec ast1 astp c)+1
+        (int_of_r_rec ast1 astp c)+1
     | a when alpha_eq(a,ast1) -> 1  
     | _ -> raise Non_closed_number
-	  
+          
 let int_of_r p =
   let (_,ast1,astp,_) = get_r_sign dummy_loc in
   try 
@@ -68,16 +69,117 @@ let replace_plus p =
      ope ("REXPR",[ope("APPLIST", [astnr; ast1; p])]) 
 
 let r_printer std_pr p =
- let (_,ast1,astp,_) = get_r_sign dummy_loc in
+  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
     | Some i -> str (string_of_int (i+1))
     | None -> std_pr (replace_plus p)
 
 let r_printer_outside std_pr p =
- let (_,ast1,astp,_) = get_r_sign dummy_loc in
+  let (_,ast1,astp,_) = get_r_sign dummy_loc in
   match (int_of_r p) with
     | Some i -> str "``" ++ str (string_of_int (i+1)) ++ str "``"
     | None -> std_pr (replace_plus p)
 
 let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
 let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside)
+
+(**********************************************************************)
+(* Parsing via scopes                                                 *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+open Bignat
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir (id_of_string id)
+
+let glob_R1 = ConstRef (make_path rdefinitions "R1")
+let glob_R0 = ConstRef (make_path rdefinitions "R0")
+let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
+let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
+
+let r_of_posint dloc n =
+  if is_nonzero n then begin
+    if Options.is_verbose () & less_than (of_string "5000") n then begin
+	warning ("You may experiment stack overflow and segmentation fault\
+                  \nwhile parsing numbers in R the absolute value of which is\
+                  \ngreater than 5000");
+	flush_all ()
+      end;
+    let ref_R1 = RRef (dloc, glob_R1) in
+    let ref_Rplus = RRef (dloc, glob_Rplus) in
+    let rec r_of_strictly_pos n =
+      if is_one n then
+        ref_R1
+      else
+        RApp(dloc, ref_Rplus, [ref_R1; r_of_strictly_pos (sub_1 n)])
+    in r_of_strictly_pos n
+  end
+  else
+    RRef (dloc, glob_R0)
+
+let check_required_module loc 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,"z_of_int",
+    str ("Cannot interpret numbers in Z without requiring first module "
+    ^(list_last d)))
+
+let r_of_int dloc z =
+  check_required_module dloc ["Coq";"Reals";"Rsyntax"];
+  match z with
+  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
+  | POS n -> r_of_posint dloc n 
+
+let _ = Symbols.declare_numeral_interpreter "R_scope" (r_of_int,None)
+
+(***********************************************************************)
+(* Printers *)
+
+exception Non_closed_number
+
+let bignat_of_pos p =
+  let (_,one,plus,_) = get_r_sign dummy_loc in
+  let rec transl = function
+    | Node (_,"APPLIST",[p; o; a]) when alpha_eq(p,plus) & alpha_eq(o,one)
+        -> add_1(transl a)
+    | a when alpha_eq(a,one) -> Bignat.one
+    | _ -> raise Non_closed_number
+  in transl p
+	  
+let bignat_option_of_pos p =
+  try 
+    Some (bignat_of_pos p)
+  with Non_closed_number -> 
+    None
+
+let r_printer_Rplus1 p =
+  match bignat_option_of_pos p with
+    | Some n -> Some (str (Bignat.to_string (add_1 n)))
+    | None -> None
+
+let r_printer_Ropp p =
+  match bignat_option_of_pos p with
+    | Some n -> Some (str "-" ++ str (Bignat.to_string n))
+    | None -> None
+
+let r_printer_R1 _ =
+  Some (int 1)
+
+let r_printer_R0 _ =
+  Some (int 0)
+
+(* Declare pretty-printers for integers *)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_Ropp" "R_scope" (r_printer_Ropp)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_Rplus1" "R_scope" (r_printer_Rplus1)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_R1" "R_scope" (r_printer_R1)
+let _ =
+  Esyntax.declare_primitive_printer "r_printer_R0" "R_scope" r_printer_R0
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index c4e94695d7..56ded08379 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -25,89 +25,42 @@ let get_z_sign loc =
     ast_of_id (id_of_string "POS"),
     ast_of_id (id_of_string "NEG")))
 
-let int_array_of_string s =
-  let a = Array.create (String.length s) 0 in
-  for i = 0 to String.length s - 1 do
-    a.(i) <- int_of_string (String.sub s i 1)
-  done;
-  a
-    
-let string_of_int_array s =
-  String.concat "" (Array.to_list (Array.map string_of_int s))
-    
-let is_nonzero a =
-  let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
-      
-let div2_with_rest n =
-  let len = Array.length n in
-  let q = Array.create len 0 in
-  for i = 0 to len - 2 do
-    q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2)
-  done;
-  q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
-  q, n.(len - 1) mod 2
-
-let add_1 n =
-  let m = Array.copy n
-  and i = ref (Array.length n - 1) in
-  m.(!i) <- m.(!i) + 1;
-  while m.(!i) = 10 && !i > 0 do
-    m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1
-  done;
-  if !i = 0 && m.(0) = 10 then begin 
-    m.(0) <- 0; Array.concat [[| 1 |]; m] 
-  end else 
-    m
-
-let rec mult_2 n =
-  let m = Array.copy n in
-  m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
-  for i = Array.length n - 2 downto 0 do
-    m.(i) <- 2 * m.(i);
-    if m.(i + 1) >= 10 then begin
-      m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1 
-    end
-  done;
-  if m.(0) >= 10 then begin 
-    m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m] 
-  end else 
-    m
-
-let pos_of_int_array astxI astxO astxH x =
+open Bignat
+
+let pos_of_bignat astxI astxO astxH x =
   let rec pos_of x =
     match div2_with_rest x with
-      | (q, 1) ->
-          if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) else astxH
-      | (q, 0) -> ope("APPLIST", [astxO; pos_of q])
-      | _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?"
+      | (q, true) when is_nonzero q -> ope("APPLIST", [astxI; pos_of q])
+      | (q, false) -> ope("APPLIST", [astxO; pos_of q])
+      | (_, true) -> astxH
   in 
   pos_of x
     
 let z_of_string pos_or_neg s dloc = 
   let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG)) = get_z_sign dloc in
-  let v = int_array_of_string s in
+  let v = Bignat.of_string s in
   if is_nonzero v then
     if pos_or_neg then
-      ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v])
+      ope("APPLIST",[astPOS; pos_of_bignat astxI astxO astxH v])
     else 
-      ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
+      ope("APPLIST",[astNEG; pos_of_bignat astxI astxO astxH v])
   else 
     astZERO
       
 exception Non_closed_number
 
-let rec int_array_of_pos c1 c2 c3 p =
+let rec bignat_of_pos c1 c2 c3 p =
   match p with
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
-        mult_2 (int_array_of_pos c1 c2 c3 a)
+        mult_2 (bignat_of_pos c1 c2 c3 a)
     | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
-        add_1 (mult_2 (int_array_of_pos c1 c2 c3 a))
-    | a when alpha_eq(a,c3) -> [| 1 |]
+        add_1 (mult_2 (bignat_of_pos c1 c2 c3 a))
+    | a when alpha_eq(a,c3) -> Bignat.one
     | _ -> raise Non_closed_number
 	  
-let int_array_option_of_pos astxI astxO astxH p =
+let bignat_option_of_pos astxI astxO astxH p =
   try 
-    Some (int_array_of_pos astxO astxI astxH p)
+    Some (bignat_of_pos astxO astxI astxH p)
   with Non_closed_number -> 
     None
 
@@ -116,35 +69,37 @@ let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a)
 
 let inside_printer posneg std_pr p =
   let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
+  match (bignat_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  (str (string_of_int_array n))
+	  (str (Bignat.to_string n))
 	else 
-	  (str "(-" ++ str (string_of_int_array n) ++ str ")")
+	  (str "(-" ++ str (Bignat.to_string n) ++ str ")")
     | None -> 
 	let pr = if posneg then pr_pos else pr_neg in
 	str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")"
 
+let outside_zero_printer std_pr p = str "`0`"
+
 let outside_printer posneg std_pr p =
   let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
-  match (int_array_option_of_pos astxI astxO astxH p) with
+  match (bignat_option_of_pos astxI astxO astxH p) with
     | Some n -> 
 	if posneg then 
-	  (str "`" ++ str (string_of_int_array n) ++ str "`")
+	  (str "`" ++ str (Bignat.to_string n) ++ str "`")
 	else 
-	  (str "`-" ++ str (string_of_int_array n) ++ str "`")
+	  (str "`-" ++ str (Bignat.to_string n) ++ str "`")
       | None -> 
 	  let pr = if posneg then pr_pos else pr_neg in
 	  str "(" ++ pr (std_pr p) ++ str ")"
 
-(* Declare pretty-printers for integers *)
+(* For printing with Syntax and without the scope mechanism *)
 let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true))
 let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false))
 let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))
 let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
 
-(* Declare the primitive parser *)
+(* Declare the primitive parser with Grammar and without the scope mechanism *)
 open Pcoq
 
 let number = create_constr_entry (get_univ "znatural") "number" 
@@ -163,3 +118,104 @@ let _ =
      [[Gramext.Stoken ("INT", "")],
       Gramext.action (z_of_string false)]]
 
+(**********************************************************************)
+(* Parsing via scopes                                                 *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let fast_integer_module = make_dir ["Coq";"ZArith";"fast_integer"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let z_path = make_path fast_integer_module (id_of_string "Z")
+let glob_z = IndRef (z_path,0)
+let glob_ZERO = ConstructRef ((z_path,0),1)
+let glob_POS = ConstructRef ((z_path,0),2)
+let glob_NEG = ConstructRef ((z_path,0),3)
+
+let positive_path = make_path fast_integer_module (id_of_string "positive")
+let glob_xI = ConstructRef ((positive_path,0),1)
+let glob_xO = ConstructRef ((positive_path,0),2)
+let glob_xH = ConstructRef ((positive_path,0),3)
+
+let pos_of_bignat dloc x =
+  let ref_xI = RRef (dloc, glob_xI) in
+  let ref_xH = RRef (dloc, glob_xH) in
+  let ref_xO = RRef (dloc, glob_xO) in
+  let rec pos_of x =
+    match div2_with_rest x with
+      | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
+      | (q,true) when is_nonzero q -> RApp (dloc,ref_xI,[pos_of q])
+      | (q,true) -> ref_xH
+  in 
+  pos_of x
+
+let z_of_string2 dloc pos_or_neg n = 
+  if is_nonzero n then
+    let sgn = if pos_or_neg then glob_POS else glob_NEG in
+    RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
+  else 
+    RRef (dloc, glob_ZERO)
+
+let check_required_module loc 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,"z_of_int",
+    str ("Cannot interpret numbers in Z without requiring first module "
+    ^(list_last d)))
+
+let z_of_int dloc z =
+  check_required_module dloc ["Coq";"ZArith";"Zsyntax"];
+  match z with
+  | POS n -> z_of_string2 dloc true n 
+  | NEG n -> z_of_string2 dloc false n 
+
+let _ = Symbols.declare_numeral_interpreter "Z_scope" (z_of_int,None)
+
+(***********************************************************************)
+(* Printers *)
+
+exception Non_closed_number
+
+let bignat_of_pos p =
+  let ((astxI,astxO,astxH),_) = get_z_sign dummy_loc in
+  let c1 = astxO in
+  let c2 = astxI in
+  let c3 = astxH in
+  let rec transl = function
+    | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c1) -> mult_2(transl a)
+    | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c2) -> add_1(mult_2(transl a))
+    | a when alpha_eq(a,c3) -> Bignat.one
+    | _ -> raise Non_closed_number
+  in transl p
+	  
+let bignat_option_of_pos p =
+  try 
+    Some (bignat_of_pos p)
+  with Non_closed_number -> 
+    None
+
+let z_printer posneg p =
+  match bignat_option_of_pos p with
+    | Some n -> 
+	if posneg then 
+	  Some (str (Bignat.to_string n))
+	else 
+	  Some (str "-" ++ str (Bignat.to_string n))
+    | None -> None
+
+let z_printer_ZERO _ =
+  Some (int 0)
+
+(* Declare pretty-printers for integers *)
+open Esyntax
+let _ =
+  declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true)
+let _ =
+  declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false)
+let _ =
+  declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO
diff --git a/parsing/symbols.ml b/parsing/symbols.ml
new file mode 100644
index 0000000000..e13fd3df4b
--- /dev/null
+++ b/parsing/symbols.ml
@@ -0,0 +1,265 @@
+open Util
+open Pp
+open Names
+open Nametab
+open Summary
+open Rawterm
+open Bignat
+
+(* A scope is a set of notations; it includes
+
+  - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
+    negative numbers (e.g. -0, -2, -13, ...). These interpreters may
+    fail if a number has no interpretation in the scope (e.g. there is
+    no interpretation for negative numbers in [nat]); interpreters both for
+    terms and patterns can be set; these interpreters are in permanent table
+    [numeral_interpreter_tab]
+  - a set of ML printers for expressions denoting numbers parsable in 
+    this scope (permanently declared in [Esyntax.primitive_printer_tab])
+  - a set of interpretations for infix (more generally distfix) notations
+  - an optional pair of delimiters which, when occurring in a syntactic
+    expression, set this scope to be the current scope
+*)
+
+let pr_bigint = function
+  | POS n -> str (Bignat.to_string n)
+  | NEG n -> str "-" ++ str (Bignat.to_string n)
+
+(**********************************************************************)
+(* Scope of symbols *)
+
+type notation = string
+type scope_name = string
+type delimiters = string * string
+type scope = {
+  notations: rawconstr Stringmap.t;
+  delimiters: delimiters option
+}
+type scopes = scope_name list
+
+(* Scopes table: scope_name -> symbol_interpretation *)
+let scope_map = ref Stringmap.empty
+
+let empty_scope = {
+  notations = Stringmap.empty;
+  delimiters = None
+}
+
+let default_scope = "core_scope"
+
+let _ = Stringmap.add default_scope empty_scope !scope_map
+
+let scope_stack = ref [default_scope]
+
+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)
+
+(* For loading without opening *)
+let declare_scope scope =
+  try let _ = Stringmap.find scope !scope_map in ()
+  with Not_found -> scope_map := Stringmap.add scope empty_scope !scope_map
+
+let declare_delimiters scope dlm =
+  let sc =
+    try Stringmap.find scope !scope_map
+    with Not_found -> empty_scope
+  in
+  if sc.delimiters <> None && Options.is_verbose () then
+    warning ("Overwriting previous delimiters in "^scope);
+  let sc = { sc with delimiters = Some dlm } in
+  scope_map := Stringmap.add scope sc !scope_map   
+
+(* The mapping between notations and production *)
+
+let declare_notation nt c scope =
+  let sc =
+    try Stringmap.find scope !scope_map
+    with Not_found -> empty_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 c sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map
+
+open Coqast
+
+let rec subst_meta_rawconstr subst = function
+  | RMeta (_,n) -> List.nth subst (n-1)
+  | t -> map_rawconstr (subst_meta_rawconstr subst) t
+
+let rec find_interpretation f = function
+  | scope::scopes ->
+      (try f (Stringmap.find scope !scope_map)
+       with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation ntn scopes args =
+  let f scope =
+    let c = Stringmap.find ntn scope.notations in
+    subst_meta_rawconstr args c in
+  try find_interpretation f scopes
+  with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+
+let find_notation_with_delimiters scope =
+  match (Stringmap.find scope !scope_map).delimiters with
+    | Some dlm -> Some (Some dlm)
+    | None -> None
+
+let rec find_notation_without_delimiters pat_scope pat = function
+  | scope::scopes ->
+      (* Is the expected printer attached to the most recently open scope? *)
+      if scope = pat_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 pat (Stringmap.find scope !scope_map).notations then
+	  find_notation_with_delimiters pat_scope
+	else
+	  find_notation_without_delimiters pat_scope pat scopes
+  | [] ->
+      find_notation_with_delimiters pat_scope
+
+let find_notation pat_scope pat scopes =
+  match 
+    find_notation_without_delimiters pat_scope pat scopes
+  with
+    | None -> None
+    | Some None -> Some (None,scopes)
+    | Some x -> Some (x,pat_scope::scopes)
+
+let exists_notation_in_scope scope ntn =
+  try Stringmap.mem ntn (Stringmap.find scope !scope_map).notations
+  with Not_found -> false
+
+let exists_notation nt =
+  Stringmap.fold (fun scn sc b -> Stringmap.mem nt sc.notations or b)
+    !scope_map false 
+
+(* TO DO
+let print_scope sc =
+  try
+    let sc = Stringmap.find scope !scope_map in
+    Stringmap.fold (fun ntn c s -> s ++ str ntn ++ Printer.pr_rawterm c)
+      sc.notations in
+  with Not_found -> str "Unknown scope"
+*)
+
+(* 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 =
+  match (Stringmap.find scope !scope_map).delimiters with
+    | Some dlm -> Some (Some dlm)
+    | None -> None
+
+let rec find_numeral_without_delimiters printer_scope = function
+  | scope :: scopes -> 
+      (* Is the expected printer attached to the most recently open scope? *)
+      if scope = printer_scope then
+	Some None
+      else
+	(* If the most recently open scope has a printer for numerals
+    	   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
+	else
+	  find_numeral_with_delimiters printer_scope
+  | [] ->
+      (* Can we switch to [scope]? Yes if it has defined delimiters *)
+      find_numeral_with_delimiters printer_scope
+
+let find_numeral_printer printer_scope scopes =
+  match 
+    find_numeral_without_delimiters printer_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)
+*)
+
+let rec interp_numeral loc n = function
+  | scope :: scopes ->
+      (try fst (lookup_numeral_interpreter scope) loc n
+       with Not_found -> interp_numeral loc n scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+let rec interp_numeral_as_pattern loc n name = function
+  | scope :: scopes ->
+      (try 
+	match snd (lookup_numeral_interpreter scope) with
+	  | None -> raise Not_found
+	  | Some g -> g loc n name
+	with Not_found -> interp_numeral_as_pattern loc n name scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral_as_pattern",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+(* Exportation of scopes *)
+let cache_scope (_,sc) =
+  if Stringmap.mem sc !scope_map then
+    scope_stack := sc :: !scope_stack
+  else
+    error ("Unknown scope: "^sc)
+
+let subst_scope (_,subst,sc) = sc
+
+open Libobject
+
+let (inScope,outScope) = 
+  declare_object {(default_object "SCOPE") with
+      cache_function = cache_scope;
+      open_function = (fun i o -> if i=1 then cache_scope o);
+      subst_function = subst_scope;
+      classify_function = (fun (_,o) -> Substitute o);
+      export_function = (fun x -> Some x) }
+
+let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
+
+(* Synchronisation with reset *)
+
+let freeze () = (!scope_map, !scope_stack)
+
+let unfreeze (scm,scs) =
+  scope_map := scm;
+  scope_stack := scs
+
+let init () = ()
+(*
+  scope_map := Strinmap.empty;
+  scope_stack := Stringmap.empty
+*)
+
+let _ = 
+  declare_summary "symbols"
+    { freeze_function = freeze;
+      unfreeze_function = unfreeze;
+      init_function = init;
+      survive_section = false }
diff --git a/parsing/symbols.mli b/parsing/symbols.mli
new file mode 100644
index 0000000000..c0d8eea294
--- /dev/null
+++ b/parsing/symbols.mli
@@ -0,0 +1,48 @@
+open Names
+open Util
+open Nametab
+open Rawterm
+open Bignat
+
+(* 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 numeral_interpreter_name = string
+type numeral_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+(* A scope is a set of interpreters for symbols + optional
+   interpreter and printers for integers + optional delimiters *)
+
+type scope_name = string
+type delimiters = string * string
+type scope
+type scopes = scope_name list
+
+val default_scope : scope_name
+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
+
+(* Declare, interpret, and look for a printer for numeral *)
+val declare_numeral_interpreter :
+  numeral_interpreter_name -> numeral_interpreter -> unit
+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 *)
+type notation = string
+val declare_notation : notation -> rawconstr -> scope_name -> unit
+val interp_notation : notation -> scopes -> rawconstr  list -> rawconstr
+val find_notation : scope_name -> notation -> scopes -> 
+  (delimiters option * scopes) option
+val exists_notation_in_scope : scope_name -> notation -> bool
+val exists_notation : notation -> bool
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 523b81b410..aee58a47ad 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Util
+open Names
 open Coqast
 open Ast
 open Extend
@@ -39,14 +40,8 @@ let _ = Pcoq.set_globalizer globalize_typed_ast
 (* This installs default quotations parsers to escape the ast parser *)
 (* "constr" is used by default in quotations found in the ast parser *) 
 let constr_parser_with_glob = Pcoq.map_entry Astterm.globalize_constr Constr.constr
-let tactic_parser_with_glob = (*map_entry Astterm.globalize_tactic*) Tactic.tactic
-let vernac_parser_with_glob = (*map_entry Astterm.globalize_vernac*) Vernac_.vernac
 
 let _ = define_quotation true "constr" constr_parser_with_glob
-(*
-let _ = define_quotation false "tactic" tactic_parser_with_glob
-let _ = define_quotation false "vernac" vernac_parser_with_glob
-*)
 
 (* Pretty-printer state summary *)
 let _ = 
@@ -107,7 +102,6 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (* Grammar rules *)
 let cache_grammar (_,a) = Egrammar.extend_grammar a
-
 let subst_grammar (_,subst,a) = Egrammar.subst_all_grammar_command subst a
 
 let (inGrammar, outGrammar) =
@@ -143,7 +137,7 @@ let print_grammar univ entry =
   let te = get_entry u entry in
   Gram.Entry.print (object_of_typed_entry te)
 
-(* Infix, distfix *)
+(* Infix, distfix, notations *)
 
 let split str =
   let rec loop beg i =
@@ -157,27 +151,39 @@ let split str =
 	loop beg (succ i)
     else if beg == i then 
       []
-    else 
+    else
       [String.sub str beg (i - beg)]
   in
   loop 0 0
 
 
-(* An infix or a distfix is a pair of a grammar rule and a pretty-printing rule
- *)
-let cache_infix (_,(gr,se)) =
-  Egrammar.extend_grammar gr;
-  Esyntax.add_ppobject {sc_univ="constr";sc_entries=se}
+(* A notation comes with a grammar rule, a pretty-printing rule, an
+   identifiying pattern called notation and an associated scope *)
+let cache_infix (_,(gr,se,ntn,scope,pat)) =
+  let b = Symbols.exists_notation_in_scope scope ntn in
+  (* Declare the printer rule and its interpretation *)
+  if not b then Esyntax.add_ppobject {sc_univ="constr";sc_entries=se};
+  (* Declare the grammar rule ... *)
+  if not (Symbols.exists_notation ntn) then Egrammar.extend_grammar gr;
+  (* ... and its interpretation *)
+  if not b then Symbols.declare_notation ntn pat scope
 
-let subst_infix (_,subst,(gr,se)) =
+let load_infix _ (_,(gr,se,ntn,scope,pat)) =
+  Symbols.declare_scope scope
+
+let subst_infix (_,subst,(gr,se,ntn,scope,pat)) =
   (Egrammar.subst_all_grammar_command subst gr,
-   list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) se)
+   list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) se,
+   ntn,
+   scope,
+   Rawterm.subst_raw subst pat)
 
 let (inInfix, outInfix) =
   declare_object {(default_object "INFIX") with
        open_function = (fun i o -> if i=1 then cache_infix o);
        cache_function = cache_infix;
        subst_function = subst_infix;
+       load_function = load_infix;
        classify_function = (fun (_,o) -> Substitute o);
        export_function = (fun x -> Some x)}
 
@@ -197,7 +203,8 @@ let constr_tab =
   [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4";
      "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "constr10" |]
   
-let constr_rule (n,p) = if p = E then constr_tab.(n) else constr_tab.(n-1)
+let constr_rule (n,p) =
+  if p = E then constr_tab.(n) else constr_tab.(max (n-1) 0)
 
 let nonterm_meta nt var =
   NonTerm(ProdPrimitive ("constr",nt), Some (var,ETast))
@@ -211,9 +218,6 @@ let collect_metas sl =
       | _ -> metatl)
     sl Pnil
 
-let make_pattern astf symbols =
-  Pnode("APPLIST",Pcons(Pquote astf, collect_metas symbols))
-
 let make_hunks symbols =
   List.fold_right
     (fun it l -> match it with
@@ -226,31 +230,25 @@ let make_hunks symbols =
 	  UNP_BRK (n, 1) :: RO s :: l)
     symbols []
 
+let string_of_symbol = function
+  | NonTerminal _ -> "_"
+  | Terminal s -> s
+
+let string_of_assoc = function
+  | Some(Gramext.RightA) -> "RIGHTA"
+  | Some(Gramext.LeftA) | None -> "LEFTA"
+  | Some(Gramext.NonA) -> "NONA"
+
+let make_symbolic assoc n symbols =
+  (string_of_assoc assoc) ^ (string_of_int n) ^
+  (String.concat " " (List.map string_of_symbol symbols))
+
 let make_production =
   List.map (function
     | NonTerminal (lp,m) -> nonterm_meta (constr_rule lp) m
     | Terminal s -> Term ("",s))
 
-let make_syntax_rule n prefname symbols astpref =
-  [{syn_id = prefname;
-    syn_prec = n,0,0;
-    syn_astpat = make_pattern astpref symbols;
-    syn_hunks = [UNP_BOX (PpHOVB 1, make_hunks symbols)]}]
-
-let make_infix_syntax_rule n prefname symbols astpref ref =
-  let hunk = match symbols with
-    | [NonTerminal ((_,lp),e1);Terminal s;NonTerminal ((_,rp),e2)] ->
-	UNP_INFIX (ref,e1,e2,(lp,rp))
-    | _ -> error "Don't know to handle this infix rule" in
-  [{syn_id = prefname;
-    syn_prec = n,0,0;
-    syn_astpat = make_pattern astpref symbols;
-    syn_hunks = [hunk]}]
-    
-
-let make_grammar_rule n fname symbols astpref =
-  let prod = make_production symbols in
-  let action = Act (PureAstPat (make_pattern astpref symbols)) in
+let make_constr_grammar_rule n fname prod action =
   Egrammar.AstGrammar
   { gc_univ = "constr";
     gc_entries =
@@ -265,59 +263,18 @@ let make_grammar_rule n fname symbols astpref =
       ]
   }
 
-let make_infix_symbols assoc n sl =
-  let (lp,rp) = prec_assoc assoc in
-  NonTerminal ((n,lp),"$a")::(List.map (fun s -> Terminal s) sl)
-  @[NonTerminal ((n,rp),"$b")]
-
-let subst_infix2 (_, subst, (ref,inf as node)) = 
-  let ref' = Libnames.subst_ext subst ref in
-    if ref' == ref then node else
-      (ref', inf)
-
-let cache_infix2 (_,(ref,inf)) =
-  let sp = match ref with
-  | Libnames.TrueGlobal r -> Nametab.sp_of_global None r
-  | Libnames.SyntacticDef kn -> Nametab.sp_of_syntactic_definition kn in
-  declare_infix_symbol sp inf
-
-let (inInfix2, outInfix2) =
-  declare_object {(default_object "INFIX2") with
-       open_function = (fun i o -> if i=1 then cache_infix2 o);
-       cache_function = cache_infix2;
-       subst_function = subst_infix2;
-       classify_function = (fun (_,o) -> Substitute o);
-       export_function = (fun x -> Some x)}
+let rec translate_implicits n = function
+  | [] -> []
+  | q::l when q=n -> true::translate_implicits (n+1) l
+  | impls -> false::translate_implicits (n+1) impls
 
-let add_infix assoc n inf (loc,qid) =
-  let ref = 
-    try
-      Nametab.extended_locate qid
-    with Not_found ->
-      error ("Unknown reference: "^(Libnames.string_of_qualid qid)) in
-  let pr = Astterm.ast_of_extended_ref_loc loc ref in
-  (* check the precedence *)
-  if n<1 or n>10 then
-    errorlabstrm "Metasyntax.infix_grammar_entry"
-      (str"Precedence must be between 1 and 10.");
-(* Pourquoi ??
-  if (assoc<>None) & (n<6 or n>9) then
-    errorlabstrm "Vernacentries.infix_grammar_entry"
-      (str"Associativity Precedence must be 6,7,8 or 9.");
-*)
-  let prefname = inf^"_infix" in
-  let symbols = make_infix_symbols assoc n (split inf) in
-  let gram_rule = make_grammar_rule n prefname symbols pr in
-  let syntax_rule = make_infix_syntax_rule n prefname symbols pr ref in
-  Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule));
-  Lib.add_anonymous_leaf (inInfix2(ref,inf))
-
-(* Distfix *)
-(* Distfix LEFTA 7 "/ _ / _ /" app.*)
-(* TODO add boxes information in the expression *)
+let implicits_of_extended_reference = function
+  | Libnames.TrueGlobal ref -> translate_implicits 1 (Impargs.implicits_of_global ref)
+  | Libnames.SyntacticDef _ -> []
 
 let create_meta n = "$e"^(string_of_int n)
 
+(*
 let rec find_symbols c_first c_next c_last new_var = function
   | []    -> []
   | ["_"] -> [NonTerminal (c_last, create_meta new_var)]
@@ -327,12 +284,160 @@ let rec find_symbols c_first c_next c_last new_var = function
   | s :: sl ->
       let symb = Terminal s in
       symb :: find_symbols c_next c_next c_last new_var sl
+*)
+let rec find_symbols c_first c_next c_last vars new_var = function
+  | []    -> (vars, [])
+  | x::sl when is_letter x.[0] ->
+      let id = Names.id_of_string x in
+      if List.mem_assoc id vars then
+        error ("Variable "^x^" occurs more than once");
+      let prec = if sl = [] then c_last else c_first in
+      let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in
+      let meta = create_meta new_var in
+      ((id,ope ("META",[num new_var]))::vars, NonTerminal (prec, meta) :: l)
+  | "_"::sl ->
+      warning "Found '_'";
+      let prec = if sl = [] then c_last else c_first in
+      let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in
+      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 new_var sl in
+      (vars, Terminal s :: l)
+
+let make_grammar_pattern symbols ntn =
+  Pnode("NOTATION",Pcons(Pquote (Str (dummy_loc,ntn)), collect_metas symbols))
+
+let make_grammar_rule n symbols ntn =
+  let prod = make_production symbols in
+  let action = Act (PureAstPat (make_grammar_pattern symbols ntn)) in
+  make_constr_grammar_rule n ("notation "^ntn) prod action
 
-let add_distfix assoc n df astf =
-  let fname = df^"_distfix" in
+let metas_of sl =
+  List.fold_right
+    (fun it metatl -> match it with
+      | NonTerminal (_,m) -> m::metatl
+      | _ -> metatl)
+    sl []
+
+let make_pattern symbols ast =
+  let env = List.map (fun m -> (m,ETast)) (metas_of symbols) in
+  fst (to_pat env ast)
+
+let make_syntax_rule n name symbols ast ntn sc =
+  [{syn_id = name;
+    syn_prec = (n,0,0);
+    syn_astpat = make_pattern symbols ast;
+    syn_hunks = [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1, make_hunks symbols))]}]
+
+let subst_meta_ast subst a =
+  let found = ref [] in
+  let rec subst_rec subst = function
+  | Smetalam (loc,s,body) -> Smetalam (loc,s,subst_rec subst body)
+  | Node(loc,"META",_) -> error "Unexpected metavariable in notation"
+  | Node(_,"QUALID",[Nvar(_,id)]) as x ->
+      (try let a = List.assoc id subst in found:=id::!found; a
+       with Not_found -> x)
+  | Node(loc,op,args) -> Node (loc,op, List.map (subst_rec subst) args)
+  | Slam(loc,None,body) -> Slam(loc,None,subst_rec subst body)
+  | Slam(loc,Some s,body) ->
+      (* Prévenir que "s" peut forcer une capturer à l'instantiation de la *)
+      (* règle de grammaire ?? *)
+      Slam(loc,Some s,subst_rec (List.remove_assoc s subst) body)
+  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
+  | Dynamic _ as a -> (* Hum... what to do here *) a
+  in
+  let a = subst_rec subst a in
+  let l = List.filter (fun (x,_) -> not (List.mem x !found)) subst in
+  if l <> [] then
+    (let x = string_of_id (fst (List.hd l)) in
+     error (x^" is unbound in the right-hand-side"));
+  a
+
+let rec reify_meta_ast = function
+  | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast body)
+  | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)
+  | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_")
+  | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast) args)
+  | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast body)
+  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
+  | Dynamic _ as a -> (* Hum... what to do here *) a
+
+(* Distfix, Infix, Notations *)
+
+let add_notation assoc n df ast sc =
+  let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
   let (lp,rp) = prec_assoc assoc in
-  let symbols = find_symbols (n,lp) (8,E) (n,rp) 0 (split df) in
-  let gram_rule = make_grammar_rule n fname symbols astf in
-  let syntax_rule = make_syntax_rule n fname symbols astf in
-  Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule))
+  let (subst,symbols) = find_symbols (n,lp) (n,L) (n,rp) [] 1 (split df) in
+  let notation = make_symbolic assoc n symbols in
+  let rule_name = notation^"_"^scope^"_notation" in
+  (* To globalize... *)
+  let vars = List.map fst subst in
+  let ast = subst_meta_ast subst ast in
+  let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars ast in
+  let ast = Termast.ast_of_rawconstr r in
+  let ast = reify_meta_ast ast in
+  let gram_rule = make_grammar_rule n symbols notation in
+  let syntax_rule = make_syntax_rule n rule_name symbols ast notation scope in
+  Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule,notation,scope,r))
 
+(* TODO add boxes information in the expression *)
+
+let inject_var x = ope ("QUALID", [nvar (id_of_string x)])
+
+let rec rename x vars n = function
+  | [] ->
+      (vars,[])
+  | "_"::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 ->
+      let (vars,l) = rename x vars n l in (vars,y::l)
+
+let add_distfix assoc n df astf sc =
+  (* "x" cannot clash since ast is globalized (included section vars) *)
+  let (vars,l) = rename "x" [] 1 (split df) in
+  let df = String.concat " " l in
+  let ast = ope("APPLIST",astf::vars) in
+  add_notation assoc n df ast sc
+
+let add_infix assoc n inf qid sc =
+  let pr = Astterm.globalize_qualid qid in
+  (* check the precedence *)
+  if n<1 or n>10 then
+    errorlabstrm "Metasyntax.infix_grammar_entry"
+      (str"Precedence must be between 1 and 10.");
+  (*
+  if (assoc<>None) & (n<6 or n>9) then
+    errorlabstrm "Vernacentries.infix_grammar_entry"
+      (str"Associativity Precedence must be 6,7,8 or 9.");
+  *)
+  let metas = [inject_var "x"; inject_var "y"] in 
+  let ast = ope("APPLIST",pr::metas) in
+  add_notation assoc n ("x "^inf^" y") ast sc
+
+(* Delimiters *)
+let cache_delimiters (_,(gram_rule,scope,dlm)) =
+  Egrammar.extend_grammar gram_rule;   (* For parsing *)
+  Symbols.declare_delimiters scope dlm (* For printing *)
+
+let load_delimiters _ (_,(gram_rule,scope,dlm)) =
+  Symbols.declare_scope scope
+
+let (inDelim,outDelim) = 
+  declare_object {(default_object "DELIMITERS") with
+      cache_function = cache_delimiters;
+      open_function = (fun i o -> if i=1 then cache_delimiters o);
+      load_function = load_delimiters;
+      export_function = (fun x -> Some x) }
+
+let add_delimiters scope (l,r as dlms) =
+  if l = "" or r = "" then error "Delimiters cannot be empty";
+  let fname = scope^"_delimiters" in
+  let symbols = [Terminal l; NonTerminal ((8,E),"$e"); Terminal r] in
+  let prod = make_production symbols in
+  let args = Pcons(Pquote (string scope), Pcons (Pmeta ("$e",Tany), Pnil)) in
+  let action = Act (PureAstPat (Pnode("DELIMITERS",args))) in
+  let gram_rule = make_constr_grammar_rule 0 fname prod action in
+  Lib.add_anonymous_leaf (inDelim(gram_rule,scope,dlms))
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 839e0fdbe9..07d1db0e3c 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Extend
 open Vernacexpr
+open Symbols
 (*i*)
 
 (* Adding grammar and pretty-printing objects in the environment *)
@@ -22,8 +23,16 @@ val add_token_obj : string -> unit
 val add_tactic_grammar :  (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> int -> string -> Libnames.qualid Util.located -> unit
+  Gramext.g_assoc option -> int -> string -> Libnames.qualid Util.located
+    -> scope_name option -> unit
 val add_distfix :
-  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t 
+    -> scope_name option -> unit
+val add_delimiters : scope_name -> delimiters -> unit
+
+val add_notation : 
+  Gramext.g_assoc option -> int -> string -> Coqast.t
+    -> scope_name option -> unit
 
 val print_grammar : string -> string -> unit
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d7a4307b22..b0f53b8393 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -285,7 +285,11 @@ let vernac_syntax = Metasyntax.add_syntax_obj
 
 let vernac_grammar = Metasyntax.add_grammar_obj
 
-let vernac_infix assoc n inf qid =
+let vernac_delimiters = Metasyntax.add_delimiters
+
+let vernac_open_scope = Symbols.open_scope
+
+let vernac_infix assoc n inf qid sc =
   let sp = sp_of_global None (global qid) in
   let dir = repr_dirpath (dirpath sp) in
 (*
@@ -295,11 +299,12 @@ let vernac_infix assoc n inf qid =
     Metasyntax.add_infix assoc n long_inf qid
   end;
 *)
-  Metasyntax.add_infix assoc n inf qid
+  Metasyntax.add_infix assoc n inf qid sc
 
-let vernac_distfix assoc n inf qid =
-  Metasyntax.add_distfix assoc n inf (Astterm.globalize_qualid qid)
+let vernac_distfix assoc n inf qid sc =
+  Metasyntax.add_distfix assoc n inf (Astterm.globalize_qualid qid) sc
 
+let vernac_notation = Metasyntax.add_notation
 
 (***********)
 (* Gallina *)
@@ -1025,8 +1030,11 @@ let interp c = match c with
   | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
   | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
   | VernacGrammar (univ,al) -> vernac_grammar univ al
-  | VernacInfix (assoc,n,inf,qid) -> vernac_infix assoc n inf qid
-  | VernacDistfix (assoc,n,inf,qid) -> vernac_distfix assoc n inf qid
+  | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
+  | VernacOpenScope sc -> vernac_open_scope sc
+  | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc
+  | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc
+  | VernacNotation (assoc,n,inf,c,sc) -> vernac_notation assoc n inf c sc
 
   (* Gallina *)
   | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d8d67a357b..e0f0dc00e4 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -14,6 +14,7 @@ open Coqast
 open Tacexpr
 open Extend
 open Genarg
+open Symbols
 
 (* Toplevel control exceptions *)
 exception ProtectedLoop
@@ -183,8 +184,14 @@ type vernac_expr =
   | VernacTacticGrammar of
       (string * (string * grammar_production list) * raw_tactic_expr) list
   | VernacSyntax of string * syntax_entry_ast list
-  | VernacInfix of grammar_associativity * int * string * qualid located
-  | VernacDistfix of grammar_associativity * int * string * qualid located
+  | VernacOpenScope of scope_name
+  | VernacDelimiters of scope_name * (string * string)
+  | VernacInfix of
+      grammar_associativity * int * string * qualid located * scope_name option
+  | VernacDistfix of
+      grammar_associativity * int * string * qualid located * scope_name option
+  | VernacNotation of
+      grammar_associativity * int * string * constr_ast * scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * identifier * definition_expr *