mise a jour

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

2 files changed, 60 insertions, 22 deletions

diff --git a/.depend b/.depend
index dbf8e04668..e8c5c9eb05 100644
--- a/.depend
+++ b/.depend
@@ -1,3 +1,4 @@
+kernel/abstraction.cmi: kernel/names.cmi kernel/term.cmi 
 kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 kernel/constant.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
@@ -8,6 +9,7 @@ kernel/generic.cmi: kernel/names.cmi lib/util.cmi
 kernel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
 kernel/inductive.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
+kernel/instantiate.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi 
 kernel/mach.cmi: kernel/environ.cmi kernel/machops.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/machops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \
@@ -27,15 +29,23 @@ lib/util.cmi: lib/pp.cmi
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 kernel/closure.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/printer.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/closure.cmi 
+    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/printer.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/closure.cmi 
 kernel/closure.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/printer.cmi kernel/term.cmx \
-    kernel/univ.cmi lib/util.cmx kernel/closure.cmi 
-kernel/environ.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi kernel/environ.cmi 
-kernel/environ.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmi kernel/environ.cmi 
+    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/printer.cmi kernel/term.cmx kernel/univ.cmi lib/util.cmx \
+    kernel/closure.cmi 
+kernel/constant.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/constant.cmi 
+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 
+kernel/environ.cmx: kernel/abstraction.cmi kernel/constant.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/univ.cmi 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 \
@@ -50,6 +60,16 @@ kernel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi lib/pp.cmi \
 kernel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx lib/pp.cmx \
     kernel/printer.cmi kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     lib/util.cmx kernel/himsg.cmi 
+kernel/inductive.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/inductive.cmi 
+kernel/inductive.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/inductive.cmi 
+kernel/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    kernel/term.cmi lib/util.cmi kernel/instantiate.cmi 
+kernel/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
+    kernel/term.cmx lib/util.cmx kernel/instantiate.cmi 
 kernel/mach.cmo: kernel/environ.cmi kernel/generic.cmi kernel/himsg.cmi \
     kernel/machops.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
@@ -59,23 +79,25 @@ kernel/mach.cmx: kernel/environ.cmx kernel/generic.cmx kernel/himsg.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/univ.cmi lib/util.cmx \
     kernel/mach.cmi 
 kernel/machops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/generic.cmi kernel/himsg.cmi kernel/inductive.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/machops.cmi 
-kernel/machops.cmx: kernel/constant.cmi kernel/environ.cmx kernel/evd.cmx \
-    kernel/generic.cmx kernel/himsg.cmx kernel/inductive.cmi kernel/names.cmx \
-    lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmi lib/util.cmx kernel/machops.cmi 
+    kernel/generic.cmi kernel/himsg.cmi kernel/inductive.cmi \
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/machops.cmi 
+kernel/machops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/himsg.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+    kernel/sign.cmx kernel/term.cmx kernel/univ.cmi lib/util.cmx \
+    kernel/machops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi 
 kernel/reduction.cmo: kernel/closure.cmi kernel/constant.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/printer.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/reduction.cmi 
-kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmi \
-    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmi \
-    kernel/names.cmx lib/pp.cmx kernel/printer.cmi kernel/term.cmx \
-    kernel/univ.cmi lib/util.cmx kernel/reduction.cmi 
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/printer.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/reduction.cmi 
+kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmx \
+    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/printer.cmi \
+    kernel/term.cmx kernel/univ.cmi lib/util.cmx kernel/reduction.cmi 
 kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \
     lib/util.cmi kernel/sign.cmi 
 kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \
diff --git a/Makefile b/Makefile
index bb2d98b367..331f8080fc 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,9 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \
     lib/dyn.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/term.cmo \
-       kernel/sign.cmo kernel/evd.cmo \
+       kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \
+       kernel/inductive.cmo \
+       kernel/environ.cmo kernel/instantiate.cmo \
        kernel/closure.cmo kernel/reduction.cmo \
        kernel/himsg.cmo kernel/machops.cmo kernel/mach.cmo
 
@@ -36,6 +38,8 @@ OBJS=$(CONFIG) $(LIB) $(KERNEL)
 
 world: $(OBJS)
 
+# Literate programming (with ocamlweb)
+
 LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL)
@@ -45,6 +49,18 @@ doc/coq.ps: doc/coq.tex
 doc/coq.tex: $(LPFILES)
 	ocamlweb -o doc/coq.tex $(LPFILES)
 
+# Emacs tags
+
+tags:
+	find . -name "*.ml*" | sort -r | xargs \
+	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
+              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
+	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
+
 # Default rules
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx