- deplacement time stamps dans System (car utilise Unix)

 - dependances fichiers camlp4 (quelle merde !)


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

3 files changed, 57 insertions, 16 deletions

diff --git a/.depend b/.depend
index 8c819d7df..1012d6900 100644
--- a/.depend
+++ b/.depend
@@ -30,7 +30,7 @@ lib/pp.cmi: lib/pp_control.cmi
 lib/util.cmi: lib/pp.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/summary.cmi: kernel/names.cmi 
-parsing/ast.cmi: lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
+parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
 parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi 
@@ -57,10 +57,12 @@ kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/constant.cmi 
 kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \
     kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/environ.cmi 
+    lib/system.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/environ.cmi 
 kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx kernel/evd.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/environ.cmi 
+    lib/system.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+    kernel/environ.cmi 
 kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
     kernel/evd.cmi 
 kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
@@ -141,6 +143,8 @@ 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/system.cmo: lib/system.cmi 
+lib/system.cmx: lib/system.cmi 
 lib/util.cmo: lib/pp.cmi lib/util.cmi 
 lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
@@ -151,10 +155,12 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
-parsing/ast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/pcoq.cmi lib/pp.cmi \
-    /usr/local/lib/camlp4/stdpp.cmi parsing/ast.cmi 
-parsing/ast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/pcoq.cmi lib/pp.cmx \
-    /usr/local/lib/camlp4/stdpp.cmi parsing/ast.cmi 
+parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
+    parsing/pcoq.cmi lib/pp.cmi /usr/local/lib/camlp4/stdpp.cmi lib/util.cmi \
+    parsing/ast.cmi 
+parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
+    parsing/pcoq.cmi lib/pp.cmx /usr/local/lib/camlp4/stdpp.cmi lib/util.cmx \
+    parsing/ast.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
@@ -169,3 +175,21 @@ toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
     kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
     /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/typing.cmx \
     lib/util.cmx 
+parsing/g_minicoq.cmo: kernel/generic.cmi /usr/local/lib/camlp4/gramext.cmi \
+    /usr/local/lib/camlp4/grammar.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/generic.cmx /usr/local/lib/camlp4/gramext.cmi \
+    /usr/local/lib/camlp4/grammar.cmi 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 /usr/local/lib/camlp4/gramext.cmi \
+    parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
+    parsing/pcoq.cmi 
+parsing/pcoq.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
+    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi lib/pp.cmi \
+    lib/util.cmi parsing/pcoq.cmi 
+parsing/pcoq.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
+    /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx lib/pp.cmx \
+    lib/util.cmx parsing/pcoq.cmi 
diff --git a/Makefile b/Makefile
index 9ffbabd46..eae9baaa2 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,3 @@
-
 # Main Makefile for Coq
 
 include config/Makefile
@@ -18,7 +17,7 @@ DEPFLAGS=$(INCLUDES)
 
 INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB)
 
-CAMLP4EXTEND=camlp4o pa_extend.cmo
+CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
 OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 
@@ -30,8 +29,8 @@ CAMLP4OBJS=gramlib.cma
 
 CONFIG=config/coq_config.cmo
 
-LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \
-    lib/dyn.cmo
+LIB=lib/pp_control.cmo lib/pp.cmo lib/system.cmo lib/util.cmo \
+    lib/hashcons.cmo lib/dyn.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \
@@ -62,9 +61,9 @@ coqtop: $(OBJS)
 MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) \
 	    parsing/lexer.cmo parsing/g_minicoq.cmo toplevel/minicoq.cmo
 
-minicoq: $(OBJS) $(MINICOQOBJS)
+minicoq: $(MINICOQOBJS)
 	$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CLIBS) $(CAMLP4OBJS) \
-	  $(OBJS) $(MINICOQOBJS) $(OSDEPLIBS)
+	  $(MINICOQOBJS) $(OSDEPLIBS)
 
 # Literate programming (with ocamlweb)
 
@@ -95,6 +94,20 @@ tags:
 parsing/lexer.cmo: parsing/lexer.ml
 	$(OCAMLC_P4O) -c $<
 
+# grammar modules with camlp4
+
+parsing/q_coqast.cmo: parsing/q_coqast.ml4
+	$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $<
+
+GRAMMAROBJS=parsing/coqast.cmo parsing/lexer.cmo parsing/pcoq.cmo \
+	    parsing/q_coqast.cmo parsing/g_prim.cmo
+
+parsing/grammar.cma: $(GRAMMAROBJS)
+	$(OCAMLC) $(BYTEFLAGS) -linkall -a -o $@
+
+parsing/g_command.cmo: parsing/g_command.ml4
+	$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $<
+
 # Default rules
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
@@ -141,8 +154,11 @@ cleanconfig::
 
 depend:
 	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
-#	for f in */*.ml4; do \
-#	  camlp4o pa_extend.cmo pr_o.cmo -impl $$f > >> .depend; \
-#	done
+	for f in */*.ml4; do \
+	  file=`dirname $$f`/`basename $$f .ml4`; \
+	  camlp4o $(INCLUDES) pa_extend.cmo pr_o.cmo -impl $$f > $$file.ml; \
+	  ocamldep $(DEPFLAGS) $$file.ml >> .depend; \
+	  rm -f $$file.ml; \
+	done
 
 include .depend
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 441d77a08..4306f3ae4 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open System
 open Util
 open Names
 open Sign