- simplification Makefile (compilation des fichiers .ml'; pas encore parfait

  car on passe par les fichiers .ml)
- Require Export enfin rétabli avec la bonne sémantique


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

8 files changed, 162 insertions, 122 deletions

diff --git a/.depend b/.depend
index 757dd9860e..6f84cc27f7 100644
--- a/.depend
+++ b/.depend
@@ -126,12 +126,13 @@ proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
 proofs/stock.cmi: kernel/names.cmi 
 proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
     kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
-    kernel/term.cmi 
+    proofs/tactic_debug.cmi kernel/term.cmi 
 proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
     proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi 
-proofs/tactic_debug.cmi: parsing/coqast.cmi proofs/proof_type.cmi 
+proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \
+    proofs/proof_type.cmi kernel/term.cmi 
 tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/names.cmi parsing/pattern.cmi \
     proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
@@ -161,7 +162,6 @@ tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi proofs/proof_type.cmi kernel/reduction.cmi \
     proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
     kernel/term.cmi 
-tactics/tauto.cmi: proofs/tacmach.cmi kernel/term.cmi 
 tactics/termdn.cmi: parsing/pattern.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \
@@ -426,12 +426,30 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
 parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernac.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    toplevel/vernac.cmx 
+parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi 
 parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi 
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/util.cmx 
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
+    lib/util.cmi toplevel/vernac.cmi 
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
+    lib/util.cmx toplevel/vernac.cmx 
 parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
     lib/util.cmi parsing/g_zsyntax.cmi 
@@ -472,6 +490,8 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/global.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     parsing/pattern.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
     parsing/termast.cmx lib/util.cmx parsing/printer.cmi 
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
     parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
     kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -724,10 +744,12 @@ proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
     kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \
     pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
-proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/tacmach.cmi proofs/tactic_debug.cmi 
-proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/tacmach.cmx proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi 
+scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
+scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
 scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
 scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx 
 tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
@@ -912,18 +934,12 @@ tactics/tactics.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
     kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
     pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \
     tactics/tactics.cmi 
-tactics/tauto.cmo: tactics/auto.cmi proofs/clenv.cmi library/declare.cmi \
-    kernel/environ.cmi tactics/hipattern.cmi kernel/names.cmi \
-    library/nametab.cmi parsing/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi tactics/tauto.cmi 
-tactics/tauto.cmx: tactics/auto.cmx proofs/clenv.cmx library/declare.cmx \
-    kernel/environ.cmx tactics/hipattern.cmx kernel/names.cmx \
-    library/nametab.cmx parsing/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx tactics/tauto.cmi 
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi 
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx 
 tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \
     pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \
@@ -936,8 +952,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi 
-tools/coqdep.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \
@@ -1075,8 +1093,8 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
     kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \
     lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \
-    kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
+    kernel/term.cmi kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
     toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \
@@ -1089,8 +1107,8 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
     proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
     kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \
     lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \
-    kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
+    kernel/term.cmx kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi toplevel/command.cmi \
     parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi kernel/names.cmi \
diff --git a/.depend.camlp4 b/.depend.camlp4
index b1c1782d10..2fb1b6be64 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,39 +1,45 @@
-parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
-parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi 
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx 
+scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
+scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
+    lib/util.cmi parsing/pcoq.cmi 
+parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
+    lib/util.cmx parsing/pcoq.cmi 
 parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
     toplevel/vernac.cmi 
 parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
     toplevel/vernac.cmx 
-parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
 parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \
     lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     parsing/g_minicoq.cmi 
-parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx 
 parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
     lib/util.cmi toplevel/vernac.cmi 
 parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
     lib/util.cmx toplevel/vernac.cmx 
-parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
-    lib/util.cmi parsing/pcoq.cmi 
-parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
-    lib/util.cmx parsing/pcoq.cmi 
-parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
-scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
-scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
+parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/util.cmx 
+parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
+parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
+    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
 toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
     lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi toplevel/mltop.cmi 
diff --git a/Makefile b/Makefile
index 1a0d3b749a..7c995fed35 100644
--- a/Makefile
+++ b/Makefile
@@ -39,10 +39,10 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
 DEPFLAGS=$(LOCALINCLUDES)
 
-CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
+CAMLP4ARGS=$(INCLUDES) pa_extend.cmo
 OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
-CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
+CAMLP4IFDEF=pa_ifdef.cmo -D$(OSTYPE)
 
 COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \
             -I theories/Init -I theories/Logic -I theories/Arith \
@@ -120,6 +120,11 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
             tactics/refine.cmo
 
 SPECTAC=tactics/tauto.ml4
+USERTAC = $(SPECTAC)
+ML4FILES += $(USERTAC)
+USERTACML=$(USERTAC:.ml4=.ml)
+USERTACCMO=$(USERTAC:.ml4=.cmo)
+USERTACCMX=$(USERTAC:.ml4=.cmx)
 
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo \
@@ -145,11 +150,11 @@ COQBINARIES= $(COQMKTOP) $(COQC) coqtop.byte $(BESTCOQTOP)
 
 world: $(COQBINARIES) states theories contrib tools
 
-coqtop.opt: $(COQMKTOP) $(CMX) user-tac-opt
+coqtop.opt: $(COQMKTOP) $(CMX) $(USERTACCMX)
 	$(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt
 	$(STRIP) ./coqtop.opt
 
-coqtop.byte: $(COQMKTOP) $(CMO) user-tac-byte Makefile
+coqtop.byte: $(COQMKTOP) $(CMO) $(USERTACCMO)
 	$(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte
 
 # coqmktop 
@@ -169,7 +174,7 @@ scripts/tolink.ml: Makefile
 	echo "let proofs = \""$(PROOFS)"\"" >> $@
 	echo "let tactics = \""$(TACTICS)"\"" >> $@
 	echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@
-	echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTAC:.ml4=.cmo)"\"" >> $@
+	echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@
 	echo "let contrib = \""$(CONTRIB)"\"" >> $@
 
 beforedepend:: scripts/tolink.ml
@@ -182,8 +187,8 @@ $(COQC): $(COQCCMO) coqtop.byte coqtop.$(BEST)
 	$(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \
 	  $(OSDEPLIBS)
 
-scripts/coqc.cmo: scripts/coqc.ml4
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $<
+scripts/coqc.ml scripts/coqc.cmo scripts/coqc.cmx: CAMLP4ARGS=$(CAMLP4IFDEF)
+ML4FILES += scripts/coqc.ml4
 
 archclean::
 	rm -f scripts/coqc scripts/coqmktop
@@ -345,19 +350,14 @@ archclean::
 # (intended to be rather generic)
 ###########################################################################
 
-USERTAC = $(SPECTAC)
-
-CAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma
-OPTCAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma \
-                   $(OSDEPP4OPTFLAGS)
+CAMLP4GRAMMAR = -I parsing pa_extend.cmo grammar.cma
 
 COQCMO = names.cmo ast.cmo g_tactic.cmo g_constr.cmo
 
-user-tac-byte: parsing/grammar.cma
-	for i in $(USERTAC); do $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done
+$(USERTACML): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
+$(USERTACCMO): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
+$(USERTACCMX): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO)
 
-user-tac-opt: parsing/grammar.cma
-	for i in $(USERTAC); do $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(OPTCAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done
 
 ###########################################################################
 # tools
@@ -481,16 +481,17 @@ beforedepend:: parsing/lexer.ml
 
 # grammar modules with camlp4
 
-parsing/q_coqast.cmo: parsing/q_coqast.ml4
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $<
+QCOQAST=parsing/q_coqast.ml4
+ML4FILES += $(QCOQAST)
+$(QCOQAST:.ml4=.ml): CAMLP4ARGS=q_MLast.cmo
+$(QCOQAST:.ml4=.cmo): CAMLP4ARGS=q_MLast.cmo
+$(QCOQAST:.ml4=.cmx): CAMLP4ARGS=q_MLast.cmo
 
-# the generic rules could be used for g_prim.ml4, but this implies
-# circular dependencies between g_prim and grammar
-parsing/g_prim.cmo: parsing/g_prim.ml4
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $<
-
-parsing/g_prim.cmx: parsing/g_prim.ml4
-	$(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $<
+GPRIM=parsing/g_prim.ml4 parsing/pcoq.ml4
+ML4FILES += $(GPRIM)
+$(GPRIM:.ml4=.ml): CAMLP4ARGS=pa_extend.cmo
+$(GPRIM:.ml4=.cmo): CAMLP4ARGS=pa_extend.cmo
+$(GPRIM:.ml4=.cmx): CAMLP4ARGS=pa_extend.cmo
 
 GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \
 	   lib/hashcons.cmo parsing/coqast.cmo parsing/lexer.cmo \
@@ -502,34 +503,28 @@ parsing/grammar.cma: $(GRAMMARCMO)
 clean::
 	rm -f parsing/grammar.cma
 
-parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $<
-
-parsing/g_%.cmx: parsing/g_%.ml4 parsing/grammar.cma
-	$(OCAMLOPT) $(OPTFLAGS) -c -pp "$(OPTCAMLP4GRAMMAR) -impl" -impl $<
-
-parsing/extend.cmo: parsing/extend.ml4 parsing/grammar.cma
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $<
-
-parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma
-	$(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $<
+PARSINGML4=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
+	   parsing/g_vernac.ml4 parsing/g_cases.ml4 \
+	   parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/extend.ml4    
+ML4FILES += $(PARSINGML4)
+$(PARSINGML4:.ml4=.ml): parsing/grammar.cma
+$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): parsing/grammar.cma
+$(PARSINGML4:.ml4=.ml): CAMLP4ARGS=$(CAMLP4GRAMMAR)
+$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): CAMLP4ARGS=$(CAMLP4GRAMMAR)
 
 beforedepend:: $(GRAMMARCMO)
 
-parsing/pcoq.ml: parsing/pcoq.ml4
-	$(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@
-
-parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma
-	$(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@
-
 beforedepend:: parsing/pcoq.ml parsing/extend.ml
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
+toplevel/mltop.ml: CAMLP4ARGS=$(CAMLP4IFDEF)
 toplevel/mltop.cmo: toplevel/mltop.ml4
-	$(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $<
+	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -DByte -impl" \
+	  -c -impl $<
 toplevel/mltop.cmx: toplevel/mltop.ml4
-	$(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $<
+	$(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -impl" -c -impl $<
+ML4FILES += toplevel/mltop.ml4
 
 ###########################################################################
 # Default rules
@@ -550,10 +545,13 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
 	ocamllex $<
 
 .ml4.cmo:
-	$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
+	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $<
 
 .ml4.cmx:
-	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
+	$(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $<
+
+.ml4.ml:
+	camlp4o pr_o.cmo $(CAMLP4ARGS) -impl $< > $@ || rm -f $@
 
 .v.vo:
 	$(COQC) -q -$(BEST) $(COQINCLUDES) $<
@@ -614,14 +612,12 @@ depend: beforedepend
 dependcoq: beforedepend
 	tools/coqdep $(COQINCLUDES) */*.v */*/*.v > .depend.coq
 
-dependcamlp4: beforedepend
-	rm -f .depend.camlp4
-	for f in */*.ml4; do \
-	  file=`dirname $$f`/`basename $$f .ml4`; \
-	  camlp4o $(INCLUDES) -I . pa_ifdef.cmo pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \
-	  ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \
-	  rm -f $$file.ml; \
-	done
+ML4FILESML = $(ML4FILES:.ml4=.ml)
+dependcamlp4: beforedepend $(ML4FILESML)
+	ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4
+
+clean::
+	rm -f $(ML4FILESML)
 
 include .depend
 include .depend.coq
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7b7c95d4bf..af46e221e2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -208,7 +208,8 @@ let unsafe_infer_type env constr =
 (* ``Type of'' machines. *)
 
 let type_of env c = 
-  let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type)
+  let (j,_) = safe_infer env c in
+  nf_betaiota env Evd.empty (body_of_type j.uj_type)
 
 (* Typing of several terms. *)
 
@@ -281,12 +282,15 @@ let add_constant_with_value sp body typ env =
 	  let (jt,cst') = safe_infer env ty in
 	  let env'' = add_constraints cst' env' in
 	  try
-	    let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in
+	    let cst'' = 
+	      conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val 
+	    in
 	    let env'' = add_constraints cst'' env'' in
 	    (env'', assumption_of_judgment env'' Evd.empty jt, 
 	     Constraint.union cst' cst'')
 	  with NotConvertible -> 
-	    error_actual_type CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val
+	    error_actual_type 
+	      CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val
   in
   let ids = 
     Idset.union (global_vars_set body) (global_vars_set (body_of_type ty))
@@ -396,7 +400,8 @@ let type_one_constructor env_ar nparams arsort c =
   let infos = 
     let (params,dc) = mind_extract_params nparams c in
     let env_par = push_rels params env_ar in
-    infos_and_sort env_par dc in
+    infos_and_sort env_par dc 
+  in
   (* Constructors are typed-checked here *)
   let (j,cst) = safe_infer_type env_ar c in
 
diff --git a/library/library.ml b/library/library.ml
index 85e9708fee..d938bd635c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -8,7 +8,7 @@ open Environ
 open Libobject
 open Lib
 
-(*s This generates commands Add Path, Remove Path, Print Path *)
+(*s Load path. Used for commands Add Path, Remove Path, Print Path *)
 
 let loadpath_name = "LoadPath"
 
@@ -77,7 +77,8 @@ let loaded_modules () =
   Stringmap.fold (fun s _ l -> s :: l) !modules_table []
 
 let opened_modules () =
-  Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l) 
+  Stringmap.fold 
+    (fun s m l -> if m.module_opened then s :: l else l) 
     !modules_table []
 
 let module_segment = function
@@ -103,12 +104,18 @@ let segment_iter f =
   iter
 
 
-(*s [open_module s] opens a module which is assumed to be already loaded. *)
+(*s [open_module s] opens a module. The module [s] and all modules needed by
+    [s] are assumed to be already loaded. When opening [s] we recursively open
+    all the modules needed by [s] and tagged [exported]. *) 
 
-let open_module s =
+let open_objects decls =
+  segment_iter open_object decls
+
+let rec open_module s =
   let m = find_module s in
   if not m.module_opened then begin
-    segment_iter open_object m.module_declarations;
+    List.iter (fun (m,_,exp) -> if exp then open_module m) m.module_deps;
+    open_objects m.module_declarations;
     m.module_opened <- true
   end
 
@@ -122,7 +129,7 @@ let open_module s =
 let load_objects decls =
   segment_iter load_object decls
 
-let rec load_module_from doexp s f =
+let rec load_module_from s f =
   let (fname,ch) = raw_intern_module (get_load_path ()) f in
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
@@ -132,32 +139,31 @@ let rec load_module_from doexp s f =
 	    module_compiled_env = md.md_compiled_env;
 	    module_declarations = md.md_declarations;
 	    module_opened = false;
-	    module_exported = doexp;
+	    module_exported = false;
 	    module_deps = md.md_deps;
 	    module_digest = digest } in
   if s <> md.md_name then
     error ("The file " ^ fname ^ " does not contain module " ^ s);
-  List.iter (load_mandatory_module doexp s) m.module_deps;
+  List.iter (load_mandatory_module s) m.module_deps;
   Global.import m.module_compiled_env;
   load_objects m.module_declarations;
   modules_table := Stringmap.add s m !modules_table;
   m
 
-and load_mandatory_module doexp caller (s,d,export) =
-  let m = find_module export s s in
+and load_mandatory_module caller (s,d,_) =
+  let m = find_module s s in
   if d <> m.module_digest then
-    error ("module "^caller^" makes inconsistent assumptions over module "^s);
-  if doexp && export then open_module s
+    error ("module "^caller^" makes inconsistent assumptions over module "^s)
 
-and find_module doexp s f =
+and find_module s f =
   try 
     Stringmap.find s !modules_table 
   with Not_found -> 
-    load_module_from doexp s f
+    load_module_from s f
 
 let load_module s = function
-  | None -> let _ = load_module_from true s s in ()
-  | Some f -> let _ = load_module_from true s f in ()
+  | None -> let _ = load_module_from s s in ()
+  | Some f -> let _ = load_module_from s f in ()
 
 
 (*s [require_module] loads and opens a module. *)
@@ -166,7 +172,7 @@ let require_module spec name fileopt export =
   let file = match fileopt with
     | None -> name
     | Some f -> f in
-  let m = load_module_from true name file in
+  let m = load_module_from name file in
   open_module name;
   if export then m.module_exported <- true
 
diff --git a/parsing/.cvsignore b/parsing/.cvsignore
index 7d96a5222d..41e9ca1c99 100644
--- a/parsing/.cvsignore
+++ b/parsing/.cvsignore
@@ -2,3 +2,10 @@ lexer.ml
 *.ppo
 pcoq.ml
 extend.ml
+g_prim.ml
+q_coqast.ml
+g_basevernac.ml
+g_vernac.ml
+g_tactic.ml
+g_constr.ml
+g_cases.ml
diff --git a/scripts/.cvsignore b/scripts/.cvsignore
index b95eb1ba95..ee865a5683 100644
--- a/scripts/.cvsignore
+++ b/scripts/.cvsignore
@@ -1,3 +1,4 @@
 coqmktop
 tolink.ml
 coqc
+coqc.ml
diff --git a/tactics/.cvsignore b/tactics/.cvsignore
new file mode 100644
index 0000000000..5ff239d459
--- /dev/null
+++ b/tactics/.cvsignore
@@ -0,0 +1 @@
+tauto.ml