Cool dev/Makefile's

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

3 files changed, 48 insertions, 10 deletions

diff --git a/dev/Makefile.devel b/dev/Makefile.devel
index 729e6147ee..ce80836ab9 100644
--- a/dev/Makefile.devel
+++ b/dev/Makefile.devel
@@ -6,22 +6,36 @@ BASEDIR=
 
 SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
 
-default:	noargument
+default:	usage noargument
 
-# set the devel makefile
+usage::
+	@echo Usage: make \<target\>
+	@echo Targets are:
+
+usage::
+	@echo "  setup-devel	-- set the devel makefile"
 setup-devel:
 	@ln -sfv dev/Makefile.devel makefile
 	@(for i in $(SOURCEDIRS); do \
 	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
 	done)
 
+
+usage::
+	@echo "  clean-devel	-- clear all devel files"
 clean-devel:
 	echo rm -f makefile .depend.devel
 	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
 
+
+usage::
+	@echo "  coqtop	-- make until the bytecode executable, make the link"
 coqtop:	bin/coqtop.byte
 	ln -sf bin/coqtop.byte coqtop
 
+
+usage::
+	@echo "  quick		-- make bytecode executable and states"
 quick: 
 	$(MAKE) states BEST=byte
 
@@ -37,10 +51,13 @@ ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
 include $(TOPDIR)/dev/Makefile.local
 endif
 
-#runs coqtop with all theories required
+usage::
+	@echo "  total		-- runs coqtop with all theories required"
 total:
 	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
 
-#runs coqtop storing using the history file
+usage::
+	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
+	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
 run:	$(TOPDIR)/coqtop
 	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
diff --git a/dev/Makefile.dir b/dev/Makefile.dir
index 163f848ad5..80fe5834c6 100644
--- a/dev/Makefile.dir
+++ b/dev/Makefile.dir
@@ -50,11 +50,13 @@ list:
 clean::  
 	rm -f *.cmi *.cmo *.cmx *.o
 
+
 # if grammar.cmo files cannot be compiled and main .depend cannot be
 # rebuilt, this is quite useful
 depend:
 	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
 
+
 # displays the dependency graph of the current directory (vertically,
 # unlike in doc/)
 graph:
@@ -95,7 +97,22 @@ pretty:	depend.ps
 #	gv -spartan $< &
 
 
-# this is not perfect bot mostly WORKS! It just calls the main makefile
+
+# generating file.ml.mli by tricking make to pass -i to ocamlc 
+
+%.ml.mli:	FORCE
+	@(cmo=`basename $@ .ml.mli`.cmo ; \
+	mv -f $$cmo $$cmo.tmp ; \
+	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
+	echo Generated interface file $@ ; \
+	mv -f $$cmo.tmp $$cmo)
+
+FORCE:
+
+clean::
+	rm -f *.ml.mli
+
+# this is not perfect but mostly WORKS! It just calls the main makefile
 
 %.cmi:	*.mli
 	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
diff --git a/dev/objects.el b/dev/objects.el
index 4e531fd7b1..46ea2dea0b 100644
--- a/dev/objects.el
+++ b/dev/objects.el
@@ -72,6 +72,10 @@ let (inThing,outThing) =
 	       ("constr option"."option_smartmap (subst_mps subst)")
 	       ("constr list"."list_smartmap (subst_mps subst)")
 	       ("constr array"."array_smartmap (subst_mps subst)")
+	       ("constr_pattern"."subst_pattern subst")
+	       ("constr_pattern option"."option_smartmap (subst_pattern subst)")
+	       ("constr_pattern array"."array_smartmap (subst_pattern subst)")
+	       ("constr_pattern list"."list_smartmap (subst_pattern subst)")
 	       ("global_reference"."subst_global subst")
 	       ("extended_global_reference"."subst_ext subst")
 	       ("obj_typ"."subst_obj subst")
@@ -93,7 +97,7 @@ let (inThing,outThing) =
     )
   )
 
-(global-set-key [f3] 'make-if)
+(global-set-key [f4] 'make-if)
 
 (defun make-record nil
   (interactive)
@@ -106,20 +110,20 @@ let (inThing,outThing) =
     )
   )
 
-(global-set-key [f4] 'make-record)
+(global-set-key [f5] 'make-record)
 
 (defun make-prim nil
   (interactive)
   (save-excursion (query-replace-regexp "\\<[a-zA-Z'_0-9]*\\>" "\\&'"))
   )
 
-(global-set-key [f5] 'make-prim)
+(global-set-key [f6] 'make-prim)
 
 
 ; eval the above, yank the text below and do 
 ; paste f2 morph.
-; paste f3 morph.
-; paste f4
+; paste f4 morph.
+; paste f5
 
       lem : constr;
       profil : bool list;