Imported Upstream version 8.1~gammaupstream/8.1.gamma

9 files changed, 76 insertions, 89 deletions

diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index 23259156..f4cb3bff 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,6 +1,27 @@
 Performance analysis for V8-0 branch
 ------------------------------------
 
+Oct 29, 2006: polymorphism on definitions (+ 4%)
+
+Oct 17, 2006: improvement in new field [r9248]
+  (QArith -3%, geometry: -2%)
+
+Oct 5, 2006: fixing wrong unification of Meta below binders
+  (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, 
+   DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%)
+
+Sep 26, 2006: new field [r9178-9181]
+  (QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it)
+
+  Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s)
+  Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s)
+  May 30, 2006: Nancy/CoLoR added (~ 319s)
+
+May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -)
+
+May 5, 2006: improvement in closure (array instead of lists)
+  (e.g. CatsInZFC: -10%, CoRN: -3%, 
+
   Dec 29, 2005: new test and use of -vm in Stalmarck
 
   Dec 27, 2005: contrib Karatsuba added (~ 30s)
diff --git a/dev/include b/dev/include
index 563edd04..42d2a017 100644
--- a/dev/include
+++ b/dev/include
@@ -25,6 +25,7 @@
 #install_printer  (* tactic *) pptac;;
 #install_printer  (* object *) ppobj;;
 #install_printer  (* global_reference *) ppglobal;;
+#install_printer  (* generic_argument *) pp_generic_argument;;
 
 #install_printer  (* fconstr *) ppfconstr;;
 
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 5c4c4475..44680d6d 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -9,20 +9,7 @@ CAMLBIN=CAMLBINDIRECTORY
 OCAMLDEBUG=$CAMLBIN/ocamldebug
 export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
 
-args=""
-coqdebug="no"
-for op in $*
-    do case `basename $op` in
-	coq-debug-programs.out) 
-	    coqdebug="yes"
-	    args="-is programs.coq";;
-	*coq*) coqdebug="yes";;
-       esac
-done
-
-case $coqdebug in
-    yes)
-	exec $OCAMLDEBUG \
+exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
 	-I $COQTOP/config \
 	-I $COQTOP/lib -I $COQTOP/kernel \
@@ -30,13 +17,12 @@ case $coqdebug in
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
 	-I $COQTOP/translate \
-        -I $COQTOP/contrib/correctness \
         -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/graphs \
+        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/first-order \
         -I $COQTOP/contrib/interface  -I $COQTOP/contrib/jprover \
         -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
         -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
 	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
-	$* $args;;
-    *) exec $OCAMLDEBUG $*;;
-esac
+        -I $COQTOP/contrib/rtauto     -I $COQTOP/contrib/setoid_ring \
+        -I $COQTOP/contrib/recdef     -I $COQTOP/contrib/dp \
+	$*
diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common
index 1ff5cf79..e69de29b 100644
--- a/dev/tools/Makefile.common
+++ b/dev/tools/Makefile.common
@@ -1,52 +0,0 @@
-# this Makefile contains goals common for directory and main devel makefiles
-
-ifndef TOPDIR
-TOPDIR=..
-endif
-
-ifndef BASEDIR
-BASEDIR=
-endif
-
-# the following entries are used to make synchronize two source trees
-# (on big computer and on a laptop for example)
-
-OTHER_FILE=$(TOPDIR)/dev/other
-OTHER=$(shell cat $(OTHER_FILE))
-
-# this is a directory of useful temporary things
-WORKDIR=tmp
-
-ifneq (,$(findstring n,$(MAKEFLAGS)))
-NFLAG=-n
-else
-NFLAG=
-endif
-
-check_other:
-	+@(if [ "$(OTHER)" = "" ] ; then \
-	  echo You must put the ssh path to the other Coq source in $(OTHER_FILE) ; \
-	  echo For example: chrzaszc@ruta:coq/V7 ; \
-	  exit 1; \
-	fi)
-
-get:	check_other
-	+rsync -Cauvz $(NFLAG) $(OTHER)/ $(TOPDIR)/
-	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
-	  rsync -auvz $(NFLAG) $(OTHER)/tmp/ $(TOPDIR)/tmp/ ; \
-	fi)
-
-put:	check_other
-	+rsync -Cauvz $(NFLAG) $(TOPDIR)/ $(OTHER)/
-	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
-	  rsync -auvz $(NFLAG) $(TOPDIR)/tmp/ $(OTHER)/tmp/ ; \
-	fi)
-
-sync:	get put
-
-
-conflicts:
-	cvs status | grep File | grep conflicts | less
-
-confl:	conflicts
-
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
index f3abb62d..8dcc70cf 100644
--- a/dev/tools/Makefile.devel
+++ b/dev/tools/Makefile.devel
@@ -16,9 +16,9 @@ usage::
 usage::
 	@echo "  setup-devel	-- set the devel makefile"
 setup-devel:
-	@ln -sfv dev/Makefile.devel makefile
+	@ln -sfv dev/tools/Makefile.devel makefile
 	@(for i in $(SOURCEDIRS); do \
-	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
+	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \
 	done)
 
 
@@ -42,14 +42,14 @@ quick:
 
 include Makefile
 
-include $(TOPDIR)/dev/Makefile.common
+include $(TOPDIR)/dev/tools/Makefile.common
 
-# this file is better described in dev/Makefile.dir
+# this file is better described in dev/tools/Makefile.dir
 include .depend.devel
 
-#if dev/Makefile.local exists, it is included
-ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
-include $(TOPDIR)/dev/Makefile.local
+#if dev/tools/Makefile.local exists, it is included
+ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),)
+include $(TOPDIR)/dev/tools/Makefile.local
 endif
 
 
@@ -71,4 +71,4 @@ usage::
 vars:
 	@(cd $(TOPDIR); \
 	echo export COQTOP=`pwd`/ ; \
-	echo export COQBIN=`pwd`/bin/ )
\ No newline at end of file
+	echo export COQBIN=`pwd`/bin/ )
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
index 68c917ac..1a1bb90b 100644
--- a/dev/tools/Makefile.dir
+++ b/dev/tools/Makefile.dir
@@ -1,6 +1,6 @@
 # make a link to this file if you are working hard in one directory of Coq
-#   ln -s ../dev/Makefile.dir Makefile
-# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+#   ln -s ../dev/tools/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead
 # this Makefile provides many useful facilities to develop Coq
 # it is not completely compatible with .ml4 files unfortunately
 
diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
index ff1f3077..cb914bd1 100644
--- a/dev/tools/Makefile.subdir
+++ b/dev/tools/Makefile.subdir
@@ -1,7 +1,7 @@
 # if you work in a sub/sub-rectory of Coq
 # you should make a link to that makefile 
-#    ln -s ../../dev/Makefile.subdir Makefile
-# in order to have all the facilities of dev/Makefile.dir
+#    ln -s ../../dev/tools/Makefile.subdir Makefile
+# in order to have all the facilities of dev/tools/Makefile.dir
 
 TOPDIR=../..
 include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 273f109c..e1ee29e4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,6 +27,8 @@ open Clenv
 open Cerrors
 open Evd
 open Goptions
+open Genarg
+
 
 let _ = Constrextern.print_evar_arguments := true
 let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
@@ -145,9 +147,9 @@ let constr_display csr =
   | Fix ((t,i),(lna,tl,bl)) ->
       "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="")
         then (";"^i) else "")) t "")^"|],"^(string_of_int i)^"),"
-      ^(array_display tl)^","
+      ^(array_display tl)^",[|"
       ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
-        then (";"^i) else "")) lna "")^","
+        then (";"^i) else "")) lna "")^"|],"
       ^(array_display bl)^")"
   | CoFix(i,(lna,tl,bl)) ->
       "CoFix("^(string_of_int i)^"),"
@@ -309,6 +311,39 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 let pploc x = let (l,r) = unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
+(* extendable tactic arguments *)
+let rec pr_argument_type = function
+  (* Basic types *)
+  | BoolArgType -> str"bool"
+  | IntArgType -> str"int"
+  | IntOrVarArgType -> str"int-or-var"
+  | StringArgType -> str"string"
+  | PreIdentArgType -> str"pre-ident"
+  | IntroPatternArgType -> str"intro-pattern"
+  | IdentArgType -> str"ident"
+  | VarArgType -> str"var"
+  | RefArgType -> str"ref"
+  (* Specific types *)
+  | SortArgType -> str"sort"
+  | ConstrArgType -> str"constr"
+  | ConstrMayEvalArgType -> str"constr-may-eval"
+  | QuantHypArgType -> str"qhyp"
+  | OpenConstrArgType _ -> str"open-constr"
+  | ConstrWithBindingsArgType -> str"constr-with-bindings"
+  | BindingsArgType -> str"bindings"
+  | RedExprArgType -> str"redexp"
+  | List0ArgType t -> pr_argument_type t ++ str" list0"
+  | List1ArgType t -> pr_argument_type t ++ str" list1"
+  | OptArgType t -> pr_argument_type t ++ str" opt"
+  | PairArgType (t1,t2) ->
+      str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
+  | ExtraArgType s -> str"\"" ++ str s ++ str "\""
+
+let pp_argument_type t = pp (pr_argument_type t)
+
+let pp_generic_argument arg =
+  pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
+
 (**********************************************************************)
 (* Vernac-level debugging commands                                    *)
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index c037eca7..1e114489 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -65,8 +65,6 @@ and ppatom a =
       print_string (string_of_kn sp);
       print_string ","; print_int i;
       print_string ")"
-  | Afix_app _ -> print_vfix_app ()
-  | Aswitch _ -> print_vswith()
 
 and ppwhd whd =
   match whd with 
@@ -74,9 +72,7 @@ and ppwhd whd =
   | Vprod _ -> print_string "product"
   | Vfun _ -> print_string "function"
   | Vfix _ -> print_vfix()
-  | Vfix_app _ -> print_vfix_app()
   | Vcofix _ -> print_string "cofix"
-  | Vcofix_app _ -> print_string "cofix_app"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
   | Vconstr_block b -> ppvblock b      
   | Vatom_stk(a,s) ->