From ab00c680d097bb067f135b0ab149b224db0787a7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Aug 1999 14:12:54 +0000
Subject: mise a jour

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@23 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3