Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

79 files changed, 745 insertions, 326 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..965adf7a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,90 @@
+*.glob
+*.d
+*.d.raw
+*.vo
+*.cm*
+*.o
+*.a
+*.annot
+*.log
+*.aux
+*.dvi
+*.blg
+*.bbl
+*.idx
+*.ilg
+*.lof
+*.toc
+*.atoc
+*.comidx
+*.comind
+*.tacidx
+*.tacind
+*.erridx
+*.errind
+*.ind
+*.hcomind
+*.htacind
+*.herrind
+*.hind
+*.haux
+*.htoc
+*.v.tex
+*.v.ps
+*.v.pdf
+*.v.html
+bin
+config/Makefile
+config/coq_config.ml
+contrib/dp/dp_zenon.ml
+contrib/micromega/csdpcert
+dev/ocamldebug-coq
+dev/ocamlweb-doc/lex.ml
+dev/ocamlweb-doc/syntax.ml
+dev/ocamlweb-doc/syntax.mli
+ide/config_lexer.ml
+ide/config_parser.ml
+ide/config_parser.mli
+ide/highlight.ml
+ide/index_urls.txt
+ide/undo.mli
+ide/utf8_convert.ml
+ide/extract_index.ml
+ide/find_phrase.ml
+kernel/copcodes.ml
+kernel/byterun/coq_jumptbl.h
+scripts/tolink.ml
+states/initial.coq
+theories/Numbers/Natural/BigN/NMake.v
+tools/coqdep_lexer.ml
+tools/coqwc.ml
+tools/gallina_lexer.ml
+tools/coqdoc/pretty.ml
+tools/coqdoc/index.ml
+toplevel/mltop.byteml
+toplevel/mltop.optml
+doc/RecTutorial/RecTutorial.html
+doc/common/version.tex
+doc/faq/html
+doc/RecTutorial/RecTutorial.pdf
+doc/RecTutorial/RecTutorial.ps
+doc/refman/Reference-Manual.html
+doc/refman/Reference-Manual.sh
+doc/refman/Reference-Manual.ps
+doc/refman/Reference-Manual.pdf
+doc/refman/coqide-queries.eps
+doc/refman/coqide.eps
+doc/refman/cover.html
+doc/refman/euclid.ml
+doc/refman/euclid.mli
+doc/refman/heapsort.ml
+doc/refman/heapsort.mli
+doc/refman/html
+doc/refman/styles.hva
+doc/stdlib/Library.coqdoc.tex
+doc/stdlib/Library.out
+doc/stdlib/Library.pdf
+doc/stdlib/Library.ps
+doc/stdlib/html/
+doc/stdlib/index-list.html
+kernel/byterun/dllcoqrun.so
diff --git a/Makefile b/Makefile
index 6854de92..6873d80c 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $ 
+# $Id: Makefile 13182 2010-06-23 09:18:18Z notin $ 
 
 
 # Makefile for Coq
@@ -24,8 +24,6 @@
 # by Emacs' next-error.
 ###########################################################################
 
-export SHELL:=/bin/bash
-
 export FIND_VCS_CLAUSE:='(' \
   -name '{arch}' -o \
   -name '.svn' -o \
@@ -183,9 +181,10 @@ docclean:
 	rm -f doc/*/*.ps doc/*/*.pdf 
 	rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
 	rm -f doc/stdlib/html/*.html
-	rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i}
+	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
+	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
 	rm -f doc/common/version.tex
-	rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
+	rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/*.eps doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
 	rm -f doc/refman/styles.hva doc/refman/cover.html 
 
diff --git a/Makefile.build b/Makefile.build
index 703c5884..148bb620 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile.build 12169 2009-06-06 21:43:23Z herbelin $ 
+# $Id: Makefile.build 12279 2009-08-14 14:54:56Z herbelin $ 
 
 
 # Makefile for Coq
@@ -447,6 +447,7 @@ install-ide-opt:
 install-ide-files:
 	$(MKDIR) $(FULLIDELIB)
 	$(INSTALLLIB) $(IDEFILES) $(FULLIDELIB)
+	if (test -f ide/index_urls.txt); then $(INSTALLLIB) ide/index_urls.txt $(FULLIDELIB); fi
 
 install-ide-info:
 	$(MKDIR) $(FULLIDELIB)
@@ -773,7 +774,7 @@ source-doc:
 
 dev/printers.cma: $(PRINTERSCMO)
 	$(SHOW)'Testing $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $(PRINTERSCMO) -o test-printer
 	@rm -f test-printer
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@
@@ -781,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO)
 parsing/grammar.cma: $(GRAMMARCMO)
 	$(SHOW)'Testing $@'
 	@touch test.ml4
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
 	@rm -f test-grammar test.*
 	$(SHOW)'OCAMLC -a $@'   
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
diff --git a/Makefile.common b/Makefile.common
index d6f43cf5..4d76e9e5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -435,7 +435,7 @@ MCHECKER:=\
 # grammar modules with camlp4
 
 GRAMMARNEEDEDCMO:=\
-  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
+  lib/profile.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
   lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo lib/predicate.cmo \
   lib/rtree.cmo lib/option.cmo \
   kernel/names.cmo kernel/univ.cmo \
diff --git a/Makefile.doc b/Makefile.doc
index 795e0e5c..f481d681 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -209,7 +209,7 @@ else
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
 endif
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
diff --git a/Makefile.stage1 b/Makefile.stage1
index c39a6372..a60d388f 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -6,7 +6,6 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-export SHELL:=/bin/bash
 include Makefile.build
 
 # All includes must be declared secondary, otherwise make will delete
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9e7a2336..24000591 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -306,7 +306,7 @@ and check_structure_field (s,env) mp lab = function
         let sub = join_alias sub (map_mp mp' mp2') in
         let sub = add_mp mp' mp2' sub in
         (join s sub, register_alias mp' mp2 env)
-      with Not_found -> failwith "unkown aliased module")
+      with Not_found -> failwith "unknown aliased module")
   | SFBmodtype mty ->
       let kn = MPdot(mp, lab) in
       check_module_type env mty;
diff --git a/config/Makefile.template b/config/Makefile.template
index 6f9fac3c..4d45f1b4 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -49,6 +49,9 @@ CAMLP4BIN="CAMLP4BINDIRECTORY"
 # Ocaml version number
 CAMLVERSION=CAMLTAG
 
+# Ocaml libraries
+CAMLLIB="CAMLLIBDIRECTORY"
+
 # Ocaml .h directory
 CAMLHLIB="CAMLLIBDIRECTORY"
 
diff --git a/configure b/configure
index 1ba4eaba..db7a55a0 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 
 ##################################
 #
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=8.2pl1
+VERSION=8.2pl2
 VOMAGIC=08200
 STATEMAGIC=58200
 DATE=`LANG=C date +"%B %Y"`
@@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then
       OK="no"
       if [ -x ./make ]; then
 	  MAKEVERSION=`./make -v | head -1`
-	  if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
+	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
       fi
       if [ $OK = "no" ]; then
 	  echo "GNU Make >= 3.81 is needed"
@@ -363,7 +363,7 @@ if [ "$browser_spec" = "no" ]; then
 fi
 
 if [ "$wwwcoq_spec" = "no" ]; then
-    WWWCOQ="http://www.lix.polytechnique.fr/coq/"
+    WWWCOQ="http://coq.inria.fr/"
 fi
 
 #########################################
@@ -665,17 +665,14 @@ esac
 
 if test "$with_doc" = "all" 
 then
-    if test "`which latex`" = ""
-    then 
-	echo "latex was not found; documentation will not be available"
-	with_doc=no
-    else
-	if test "`which hevea`" = ""
-	then
+    for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do
+	if test ! -x "`which $cmd`"
+	then 
+	    echo "$cmd was not found; documentation will not be available"
 	    with_doc=no
-	    echo "hevea was not found: documentation will not be available"
+	    break
 	fi
-    fi
+    done
 fi
 
 ###########################################
@@ -1080,4 +1077,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 12219 2009-07-01 09:58:00Z notin $
+# $Id: configure 13223 2010-06-29 18:28:35Z notin $
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 79ffaf3f..d8803847 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -701,7 +701,7 @@ let file_contents f =
 let timeout_sys_command cmd =
   if !debug then Format.eprintf "command line: %s@." cmd;
   let out = Filename.temp_file "out" "" in
-  let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+  let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
   let ret = Sys.command cmd in
   if !debug then 
     Format.eprintf "Output file %s:@.%s@." out (file_contents out);
@@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f])
 
 let call_simplify fwhy =
   let cmd = 
-    sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy) 
+    sprintf "why --simplify %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
   let cmd = 
-    sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out" 
+    sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
       !timeout fsx
   in
   let out = Sys.command cmd in
@@ -747,7 +747,7 @@ let call_simplify fwhy =
   r
 
 let call_ergo fwhy =
-  let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+  let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
   let ftrace = Filename.temp_file "ergo_trace" "" in
@@ -797,12 +797,12 @@ let call_zenon fwhy =
 
 let call_yices fwhy =
   let cmd = 
-    sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+    sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
   let cmd = 
-    sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out" 
+    sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
       !timeout fsmt
   in
   let out = Sys.command cmd in
@@ -814,7 +814,7 @@ let call_yices fwhy =
 
 let call_cvcl fwhy =
   let cmd = 
-    sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+    sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
@@ -831,7 +831,7 @@ let call_cvcl fwhy =
 
 let call_harvey fwhy =
   let cmd = 
-    sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+    sprintf "why --harvey --encoding strat %s" (why_files fwhy)
   in
   if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
   let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
@@ -856,7 +856,7 @@ let call_harvey fwhy =
   r
 
 let call_gwhy fwhy =
-  let cmd = sprintf "gwhy --no-arrays  %s" (why_files fwhy) in
+  let cmd = sprintf "gwhy %s" (why_files fwhy) in
   if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
   NoAnswer
 
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 02173c1f..73f44e68 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
+(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
 
 open Pp
 open Util
@@ -21,6 +21,8 @@ open Mlutil
 open Modutil
 open Mod_subst
 
+let string_of_id id = ascii_of_ident (Names.string_of_id id)
+
 (*s Some pretty-print utility functions. *)
 
 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -73,7 +75,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
 let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+let uppercase_id id =
+  let s = string_of_id id in
+  assert (s<>"");
+  if s.[0] = '_' then id_of_string ("Coq_"^s)
+  else id_of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 49a86200..057a7b29 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*)
+(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -489,15 +489,12 @@ let simple_extraction r = match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
       init false;
-      if is_custom r then
-	msgnl (str "User defined extraction:" ++ spc () ++
-		 str (find_custom r) ++ fnl ())
-      else
-	let struc = optimize_struct [r] (mono_environment [r] []) in
-	let d = get_decl_in_structure r struc in
-	warning_axioms ();
-	print_one_decl struc (modpath_of_r r) d;
-	reset ()
+      let struc = optimize_struct [r] (mono_environment [r] []) in
+      let d = get_decl_in_structure r struc in
+      warning_axioms ();
+      if is_custom r then msgnl (str "(** User defined extraction *)");
+      print_one_decl struc (modpath_of_r r) d;
+      reset ()
   | _ -> assert false
 
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 79aeea33..4e2904ba 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*)
+(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -578,7 +578,7 @@ let eta_red e =
 	  if m = n then 
 	    [], f, a
 	  else if m < n then 
-	    snd (list_chop (n-m) ids), f, a 
+	    list_skipn m ids, f, a
 	  else (* m > n *)
 	    let a1,a2 = list_chop (m-n) a in 
 	    [], MLapp (f,a1), a2
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 6dc0d5bf..14bf7cf8 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: recdef.ml 12221 2009-07-04 21:53:12Z jforest $ *)
 
 open Term
 open Termops
@@ -960,11 +960,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		       let ids' = pf_ids_of_hyps g in 
 		       lid := List.rev (list_subtract ids' ids);
 		       if !lid = [] then lid := [hid];
-(* 		       list_iter_i  *)
-(* 			 (fun i v ->  *)
-(* 			    msgnl (str "hyp" ++ int i ++ str " " ++  *)
-(* 				     Nameops.pr_id v ++ fnl () ++ fnl())) *)
-(* 			      !lid; *)
 		       tclIDTAC g
 		    )
 		    g
@@ -976,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       Auto.h_auto None [] (Some [])  g
 	   | _ ->
 	       incr h_num;
-	       tclTHEN
-		 (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
-		 e_assumption
+	       (observe_tac "finishing using"
+		  (
+		    tclCOMPLETE(
+		      tclFIRST[
+			tclTHEN
+			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+			  e_assumption;			  
+		      Eauto.eauto_with_bases
+			false
+			(true,5)
+			[delayed_force refl_equal]
+			[Auto.Hint_db.empty empty_transparent_state false]
+		      ]
+		    )
+		  )
+	       ) 
       		 g)
 ;
     Command.save_named opacity;
diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index e2d04cb7..5b217119 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -70,7 +70,7 @@ let pp strm fn =
       let ch = open_out filename in
        pp_ch strm ch;
        close_out ch ;
-       print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
+       print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n");
        flush stdout
    | None ->
        pp_ch strm stdout
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1ae18661..f4719594 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -662,21 +662,21 @@ let _ =
          | Some fn ->
             let ch = open_out (fn ^ ".v") in
              Buffer.output_buffer ch theory_buffer ;
+             close_out ch;
+            (* dummy glob file *)
+            let ch = open_out (fn ^ ".glob") in
              close_out ch
        end ;
        Option.iter 
 	(fun fn ->
 	  let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
-	  let dir = Option.get xml_library_root in
           let command cmd =
            if Sys.command cmd <> 0 then
             Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
           in
-           command (coqdoc^options^" -d "^dir^" "^fn^".v");
-           let dot = if fn.[0]='/' then "." else "" in
-           command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
-           command ("rm "^fn^".v");
+           command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
+           command ("rm "^fn^".v "^fn^".glob");
            print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
        ofn)
 ;;
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 560d06d9..5f49561b 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -19,7 +19,7 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
         -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
         -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/firstorder \
-        -I $COQTOP/contrib/interface \
+        -I $COQTOP/contrib/interface  -I $COQTOP/contrib/cc \
         -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
         -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
 	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
diff --git a/dev/v8-syntax/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc5..194a55fe 100755
--- a/dev/v8-syntax/check-grammar
+++ b/dev/v8-syntax/check-grammar
@@ -1,31 +1,31 @@
-#!/bin/bash
+#!/bin/sh
 # This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
 # is consistent in the sense that all invoked non-terminals are defined
 
-defined-nt() {
+defined_nt() {
   grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
     sort | sort -u
 }
 
-used-nt() {
+used_nt() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
     sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
 }
 
-used-term() {
+used_term() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
     sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
 }
 
-used-kwd() {
+used_kwd() {
   cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
     sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
 }
 
-defined-nt > def
-used-nt > use
-used-term > use-t
-used-kwd > use-k
+defined_nt > def
+used_nt > use
+used_term > use-t
+used_kwd > use-k
 diff def use > df
 
 ###############################
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index 916a06e9..4488b5e9 100644
--- a/ide/undo_lablgtk_ge212.mli
+++ b/ide/undo_lablgtk_ge212.mli
@@ -10,9 +10,10 @@
 
 (* An undoable view class *)
 
-class undoable_view : [> Gtk.text_view] Gtk.obj ->
+class undoable_view : ([> Gtk.text_view] as 'a) Gtk.obj ->
 object
   inherit GText.view
+  val obj : 'a Gtk.obj
   method undo : bool
   method redo : bool
   method clear_undo : unit
diff --git a/install.sh b/install.sh
index c2f8215b..277222f5 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/bash
+#! /bin/sh
 
 dest="$1"
 shift
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f99af68e..99bcf159 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: constrextern.ml 12495 2009-11-11 12:10:44Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -363,7 +363,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v =
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | PatVar (_,Anonymous), AHole _ -> sigma
-  | a, AHole _ -> sigma
   | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
       let nparams =
 	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8d6a92a2..c8faf911 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
 
 open Pp
 open Util
@@ -450,8 +450,8 @@ let rec simple_adjust_scopes n = function
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
   let npar = mib.Declarations.mind_nparams in
-  snd (list_chop (List.length pl1 + npar)
-    (simple_adjust_scopes (npar + List.length pl2)
+  snd (list_chop (npar + List.length pl1)
+    (simple_adjust_scopes (npar + List.length pl1 + List.length pl2)
       (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
@@ -526,6 +526,7 @@ let error_invalid_pattern_notation loc =
 
 let chop_aconstr_constructor loc (ind,k) args =
   let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  if nparams > List.length args then error_invalid_pattern_notation loc;
   let params,args = list_chop nparams args in
   List.iter (function AHole _ -> ()
     | _ -> error_invalid_pattern_notation loc) params;
@@ -728,8 +729,7 @@ let locate_if_isevar loc na = function
 let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
     errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
-    pr_id id ++ strbrk " must not be used as a bound variable in the type \
-of its constructor.")
+    pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
 let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
   | Anonymous -> 
@@ -1060,15 +1060,17 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
-        let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = Option.map (intern_type env'') po in
+        let p' = Option.map (fun p ->
+          let env'' = List.fold_left (push_name_env lvar) env ids in
+	  intern_type env'' p) po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
-        let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = Option.map (intern_type env'') po in
+        let p' = Option.map (fun p ->
+          let env'' = List.fold_left (push_name_env lvar) env ids in
+	  intern_type env'' p) po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) -> 
 	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
@@ -1147,6 +1149,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	[], None in
     let na = match tm', na with
       | RVar (_,id), None when Idset.mem id vars -> Name id
+      | RRef (loc, VarRef id), None -> Name id
       | _, None -> Anonymous
       | _, Some na -> na in
     (tm',(na,typ)), na::ids
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 06764834..941ab046 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: indtypes.ml 12616 2009-12-30 15:02:26Z herbelin $ *)
 
 open Util
 open Names
@@ -494,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
 		  raise (IllFormedInd LocalNotConstructor)
 	      else
 		if not (List.for_all (noccur_between n ntypes) largs)
-              then raise (IllFormedInd (LocalNonPos n));
+		then failwith_non_pos_list n ntypes largs;
 	      (nmr,List.rev lrec)
     in check_constr_rec ienv nmr [] c
   in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 949a7402..34d9e930 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
+(*i $Id: modops.ml 12234 2009-07-09 09:14:09Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -143,11 +143,13 @@ let rec subst_with_body sub = function
 
 and subst_modtype sub mtb =
   let typ_expr' = subst_struct_expr sub mtb.typ_expr in
-    if typ_expr'==mtb.typ_expr then
+  let sub_mtb = join_alias mtb.typ_alias sub in
+    if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then
       mtb
     else
       { mtb with 
-	  typ_expr = typ_expr'}
+	  typ_expr = typ_expr';
+	  typ_alias = sub_mtb}
 	
 and subst_structure sub sign = 
   let subst_body  = function
diff --git a/lib/system.ml b/lib/system.ml
index 65826c81..3fa32ef8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -153,8 +153,12 @@ let where_in_path ?(warn=true) path filename =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
-    let root = Filename.dirname filename in
-    root, filename
+    if Sys.file_exists filename then
+      let root = Filename.dirname filename in
+      root, filename
+    else
+      errorlabstrm "System.find_file_in_path"
+	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else 
     try where_in_path ~warn paths filename
     with Not_found ->
@@ -224,6 +228,13 @@ let extern_intern ?(warn=true) magic suffix =
   in 
   (extern_state,intern_state)
 
+let with_magic_number_check f a =
+  try f a
+  with Bad_magic_number fname ->
+    errorlabstrm "with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ 
+    strbrk "It is corrupted or was compiled with another version of Coq.")
+
 (* Communication through files with another executable *)
 
 let connect writefun readfun com =
diff --git a/lib/system.mli b/lib/system.mli
index ba5aa408..426a00df 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
+(*i $Id: system.mli 13175 2010-06-22 06:28:37Z herbelin $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
@@ -54,6 +54,8 @@ val raw_extern_intern : int -> string ->
 val extern_intern : ?warn:bool -> int -> string -> 
   (string -> 'a -> unit) * (load_path -> string -> 'a)
 
+val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
+
 (*s Sending/receiving once with external executable *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a 
diff --git a/lib/util.ml b/lib/util.ml
index dce36419..0d6e7ff2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *)
+(* $Id: util.ml 13200 2010-06-25 22:36:25Z letouzey $ *)
 
 open Pp
 
@@ -486,6 +486,26 @@ let lowercase_first_char_utf8 s =
   let j, n = next_utf8 s 0 in
   utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n)
 
+(* For extraction, we need to encode unicode character into ascii ones *)
+
+let ascii_of_ident s =
+  let check_ascii s =
+    let ok = ref true in
+    String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
+    !ok
+  in
+  if check_ascii s then s else
+    let i = ref 0 and out = ref "" in
+    begin try while true do
+      let j, n = next_utf8 s !i in
+      out :=
+       if n >= 128
+       then Printf.sprintf "%s__U%04x_" !out n
+       else Printf.sprintf "%s%c" !out s.[!i];
+      i := !i + j
+    done with End_of_input -> () end;
+    !out
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
diff --git a/lib/util.mli b/lib/util.mli
index 5432eb98..97bda074 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
+(*i $Id: util.mli 13200 2010-06-25 22:36:25Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -94,6 +94,7 @@ val classify_unicode : int -> utf8_status
 val check_ident : string -> unit
 val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
+val ascii_of_ident : string -> string
 
 (*s Lists. *)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 93021384..cfada00c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
+(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -851,8 +851,7 @@ let classify_import (_,(export,_ as obj)) =
   if export then Substitute obj else Dispose
 
 let subst_import (_,subst,(export,mp as obj)) =
-  let subst' = remove_alias subst in
-  let mp' = subst_mp subst' mp in
+  let mp' = subst_mp subst mp in
     if mp'==mp then obj else
       (export,mp')
 	
diff --git a/library/goptions.ml b/library/goptions.ml
index a9b33235..8625ee52 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id: goptions.ml 13196 2010-06-25 18:01:50Z herbelin $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -297,10 +297,11 @@ let set_int_option_value = set_option_value
   (fun v -> function 
      | (IntValue _) -> IntValue v
      | _ -> bad_type_error ())
-let set_bool_option_value = set_option_value
-  (fun v -> function 
+let set_bool_option_value key v =
+  try set_option_value (fun v -> function
      | (BoolValue _) -> BoolValue v
-     | _ -> bad_type_error ())
+     | _ -> bad_type_error ()) key v
+  with UserError (_,s) -> Flags.if_verbose msg_warning s
 let set_string_option_value = set_option_value
  (fun v -> function 
     | (StringValue _) -> StringValue v
diff --git a/library/lib.ml b/library/lib.ml
index 4a124cec..f0ec488b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: lib.ml 12496 2009-11-11 13:37:57Z herbelin $ *)
 
 open Pp
 open Util
@@ -171,9 +171,8 @@ let find_split_p p =
 
 let split_lib_gen test = 
   let rec collect after equal = function
-    | hd::strict_before as before ->
-      	if test hd then collect after (hd::equal) strict_before else after,equal,before
-    | [] as before -> after,equal,before
+    | hd::before when test hd -> collect after (hd::equal) before
+    | before -> after,equal,before
   in
   let rec findeq after = function
     | hd :: before ->
@@ -194,7 +193,14 @@ let split_lib_gen test =
       | None -> error "no such entry"
       | Some r -> r
 
-let split_lib sp = split_lib_gen (fun x -> (fst x) = sp)
+let split_lib sp = split_lib_gen (fun x -> fst x = sp)
+
+let split_lib_at_opening sp =
+  split_lib_gen (function
+    | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) ->
+	x = sp
+    | _ ->
+	false)
 
 (* Adding operations. *)
 
@@ -299,7 +305,7 @@ let end_module id =
     with Not_found ->
       error "no opened modules"
   in
-  let (after,modopening,before) = split_lib oname in
+  let (after,modopening,before) = split_lib_at_opening oname in
   lib_stk := before;
   add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
   let prefix = !path_prefix in
@@ -344,7 +350,7 @@ let end_modtype id =
     with Not_found ->
       error "no opened module types"
   in
-  let (after,modtypeopening,before) = split_lib sp in
+  let (after,modtypeopening,before) = split_lib_at_opening sp in
   lib_stk := before;
   add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
   let dir = !path_prefix in
@@ -407,7 +413,7 @@ let end_compilation dir =
 	    ("The current open module has name "^ (Names.string_of_dirpath m) ^ 
 	       " and not " ^ (Names.string_of_dirpath m));
   in
-  let (after,_,before) = split_lib oname in
+  let (after,_,before) = split_lib_at_opening oname in
     comp_name := None;
     !path_prefix,after
 
@@ -587,7 +593,7 @@ let close_section id =
     with Not_found ->
       error "No opened section."
   in
-  let (secdecls,secopening,before) = split_lib oname in
+  let (secdecls,secopening,before) = split_lib_at_opening oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
@@ -640,7 +646,7 @@ let reset_to_gen test =
   let (_,_,before) = split_lib_gen test in
   set_lib_stk before
 
-let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
+let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
 let reset_to_state sp =
   let (_,eq,before) = split_lib sp in
@@ -667,7 +673,7 @@ let delete_gen test =
  in
   set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
 
-let delete sp = delete_gen (fun x -> (fst x) = sp)
+let delete sp = delete_gen (fun x -> fst x = sp)
 
 let reset_name (loc,id) =
   let (sp,_) = 
diff --git a/library/library.ml b/library/library.ml
index 0e1342f0..2c6d02ae 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -328,14 +328,6 @@ let (in_import, out_import) =
 let (raw_extern_library, raw_intern_library) =
   System.raw_extern_intern Coq_config.vo_magic_number ".vo"
 
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
-
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
@@ -414,7 +406,7 @@ let mk_library md digest = {
   library_digest = digest }
 
 let intern_from_file f =
-  let ch = with_magic_number_check raw_intern_library f in
+  let ch = System.with_magic_number_check raw_intern_library f in
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
   close_in ch;
diff --git a/library/states.ml b/library/states.ml
index c81f9614..3a4be1ca 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
+(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open System
 
@@ -24,7 +24,8 @@ let (extern_state,intern_state) =
     extern_intern Coq_config.state_magic_number ".coq" in
   (fun s -> raw_extern s (freeze())),
   (fun s ->
-    unfreeze (raw_intern (Library.get_load_paths ()) s);
+    unfreeze
+      (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
     Library.overwrite_library_filenames s)
 
 (* Rollback. *)
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 45fcafd2..e07ccdd3 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -75,7 +75,7 @@ Considers the file `file' respectively as a .v (or .g) file or a .tex file.
 .TP
 .BI \-\-files\-from \ file
 Read file names to process in file `file' as if they were given on the
-command line. Useful for program sources splitted in several
+command line. Useful for program sources split in several
 directories.
 .TP
 .B \-q, \ \-\-quiet
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 61c3474d..35fc064b 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *)
 
 
 open Decl_expr
@@ -220,7 +220,7 @@ GLOBAL: proof_instr;
   intro_step:
     [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
      | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
-       po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; 
+       po=OPT[ "with"; p=LIST1 hyp SEP ","-> p  ] ; 
        ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
 	 Pcase (none_is_empty po,c,none_is_empty ho)
      | "let" ; v=let_vars -> Plet v	 
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index a589ccf1..64fa0b49 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: g_intsyntax.ml 12509 2009-11-12 15:52:50Z letouzey $ i*)
 
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
@@ -92,13 +92,15 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
 
 (*bigQ stuff*)
 let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
-let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"]
+let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake"]
 let bigQ_path = make_path (bigQ_module@["BigQ"]) "t"
 (* big ugly hack bis *)
-let bigQ_id = make_kn qmake_module
+let bigQ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigQ_module)), 
+                             Names.mk_label "BigQ")),
+              [], Names.id_of_string id) : Names.kernel_name)
 let bigQ_scope = "bigQ_scope"
 
-let bigQ_z =  ConstructRef ((bigQ_id "q_type",0),1)
+let bigQ_z =  ConstructRef ((bigQ_id "t_",0),1)
 
 
 (*** Definition of the Non_closed exception, used in the pretty printing ***)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b2d67e1c..f727dfea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *)
 
 
 open Pp
@@ -663,6 +663,8 @@ GEXTEND Gram
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Compute"; c = lconstr ->
+	  fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c)
       | IDENT "Check"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 2633386f..52b5ede7 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*)
+(*i $Id: lexer.ml4 12891 2010-03-30 11:40:02Z herbelin $ i*)
 
 
 (*i camlp4use: "pr_o.cmo" i*) 
@@ -91,6 +91,14 @@ let error_utf8 cs =
   Stream.junk cs; (* consume the char to avoid read it and fail again *)
   err (bp, bp+1) Illegal_character
 
+let utf8_char_size cs = function
+  (* Utf8 leading byte *)
+  | '\x00'..'\x7F' -> 1
+  | '\xC0'..'\xDF' -> 2
+  | '\xE0'..'\xEF' -> 3
+  | '\xF0'..'\xF7' -> 4
+  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs
+
 let njunk n = Util.repeat n Stream.junk
 
 let check_utf8_trailing_byte cs c =
@@ -355,14 +363,8 @@ and progress_utf8 last nj n c tt cs =
   with Not_found ->
     last
 
-and progress_from_byte last nj tt cs = function
-  (* Utf8 leading byte *)
-  | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
-  | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
-  | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
-  | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
-  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
-      error_utf8 cs
+and progress_from_byte last nj tt cs c =
+  progress_utf8 last nj (utf8_char_size cs c) c tt cs
 
 (* Must be a special token *)
 let process_chars bp c cs =
@@ -370,7 +372,10 @@ let process_chars bp c cs =
   let ep = Stream.count cs in
   match t with
     | Some t -> (("", t), (bp, ep))
-    | None -> err (bp, ep) Undefined_token
+    | None ->
+	let ep' = bp + utf8_char_size cs c in
+	njunk (ep' - ep) cs;
+	err (bp, ep') Undefined_token
 
 let parse_after_dollar bp =
   parser
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3b433498..f52ebc76 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *)
 
 open Pp
 open Names
@@ -378,7 +378,7 @@ let pr_as_ipat = function
 
 let pr_as_name = function
   | Anonymous -> mt ()
-  | Name id -> str "as " ++ pr_lident (dummy_loc,id)
+  | Name id -> str " as " ++ pr_lident (dummy_loc,id)
 
 let pr_pose_as_style prc na c =
   spc() ++ prc c ++ pr_as_name na
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2d8921e..abe4fcc1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
+(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *)
 
 open Util
 open Names
@@ -851,7 +851,7 @@ let rec map_predicate f k ccl = function
   | Abstract _ :: rest ->
       map_predicate f (k+1) ccl rest
 
-let noccurn_predicate = map_predicate noccurn
+let noccur_predicate_between n = map_predicate (noccur_between n)
 
 let liftn_predicate n = map_predicate (liftn n)
 
@@ -1122,13 +1122,16 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
   (* into  "Gamma; typs; curalias |- tms" *)
   let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
 
+  let pred_is_not_dep =
+    noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
+
   let typs'' = 
     list_map2_i
       (fun i (na,t) deps ->
 	let dep = match dep with
 	  | Name _ as na',k -> (if na <> Anonymous then na else na'),k
 	  | Anonymous,KnownNotDep ->
-	      if deps = [] && noccurn_predicate 1 pb.pred tomatch then
+	      if deps = [] && pred_is_not_dep then
 		(Anonymous,KnownNotDep)
 	      else
 		(force_name na,KnownDep)
@@ -1801,7 +1804,8 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 	   let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in
            let arsign = extract_arity_signature env tomatchs sign in
            let names2 = List.rev (List.map (List.map pi1) arsign) in
-	   let nal2,pred2 = build_initial_predicate KnownNotDep names2 t2 in
+           let pred2 = lift (List.length names2) t2 in
+	   let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in
 	   [evdref, nal1, pred1; evdref2, nal2, pred2])
 
   (* Some type annotation *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 51952f4f..0bfef04a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: clenv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -410,8 +410,9 @@ let clenv_unify_binding_type clenv c t u =
     try
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
-    with e when precatchable_exception e ->
-      TypeNotProcessed, clenv, c
+    with
+      | PretypeError (_,NotClean _) as e -> raise e
+      | e when precatchable_exception e -> TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
@@ -436,11 +437,11 @@ let clenv_match_args bl clenv =
 	  clenv_assign_binding clenv k sc)
       clenv bl
 
+exception NoSuchBinding
+
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
-  let k =
-    try list_last all_mvs 
-    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
+  let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k (Evd.empty,c)
 
 let clenv_constrain_dep_args hyps_only bl clenv =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9b2d6e29..4c5535b3 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*)
+(*i $Id: clenv.mli 13126 2010-06-13 11:09:51Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -94,6 +94,8 @@ type arg_bindings = open_constr explicit_bindings
 val clenv_independent : clausenv -> metavariable list
 val clenv_missing : clausenv -> metavariable list
 
+(** for the purpose of inversion tactics *)
+exception NoSuchBinding
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
 (* defines metas corresponding to the name of the bindings *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73dc5d46..20cbba94 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *)
 
 open Pp
 open Util
@@ -329,7 +329,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let eqnl = detype_eqns constructs consnargsl bl in
   let tag =
     try 
       if !Flags.raw_print then
@@ -357,8 +356,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	RIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
+	let eqnl = detype_eqns constructs consnargsl bl in
 	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
+      let eqnl = detype_eqns constructs consnargsl bl in
       RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 043a326d..18e79e85 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
+(* $Id: evarconv.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
 
 open Pp
 open Util
@@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c =
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
+let position_problem l2r = function
+  | CONV -> None
+  | CUMUL -> Some l2r
+
 (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
    (t1 l1) = (t2 l2) into a problem
 
@@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 =
         let term1 = apprec_nohdbeta env evd term1 in
         let term2 = apprec_nohdbeta env evd term2 in
         if is_undefined_evar evd term1 then
-          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+          solve_simple_eqn evar_conv_x env evd
+	    (position_problem true pbty,destEvar term1,term2)
         else if is_undefined_evar evd term2 then
-          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
+          solve_simple_eqn evar_conv_x env evd
+	    (position_problem false pbty,destEvar term2,term1)
         else
           evar_eqappr_x env evd pbty
             (decompose_app term1) (decompose_app term2)
@@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
               [(fun i -> solve_simple_eqn evar_conv_x env i
-	        (pbty,ev2,applist(term1,deb1)));
+	        (position_problem false pbty,ev2,applist(term1,deb1)));
               (fun i -> ise_list2 i
                   (fun i -> evar_conv_x env i CONV) rest1 l2)]
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
             ise_and i
               [(fun i -> solve_simple_eqn evar_conv_x env i
-	          (pbty,ev1,applist(term2,deb2)));
+	          (position_problem true pbty,ev1,applist(term2,deb2)));
               (fun i -> ise_list2 i
                   (fun i -> evar_conv_x env i CONV) l1 rest2)]
 	and f2 i =
@@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar (evars_of evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+	    solve_simple_eqn evar_conv_x env evd
+	      (position_problem true pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
 	  then
@@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar (evars_of evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+	    solve_simple_eqn evar_conv_x env evd
+	      (position_problem false pbty,ev2,t1)
 	  else if
        	    List.length l2 <= List.length l1
 	  then
@@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t2 = nf_evar (evars_of evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+	  solve_simple_eqn evar_conv_x env evd
+	    (position_problem true pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t1 = nf_evar (evars_of evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+	  solve_simple_eqn evar_conv_x env evd
+	    (position_problem false pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -505,7 +515,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       if is_defined_evar i ev1 then
 	evar_conv_x env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
+	solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 994da427..fbaac79b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
+(* $Id: evarutil.ml 13116 2010-06-12 15:18:07Z herbelin $ *)
 
 open Util
 open Pp
@@ -113,11 +113,27 @@ let push_dependent_evars sigma emap =
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
 
+let push_duplicated_evars sigma emap c	=
+  let rec collrec (one,(sigma,emap) as acc) c =
+    match kind_of_term c with
+    | Evar (evk,_) when not (Evd.mem sigma evk) ->
+       if List.mem evk one then
+         let sigma' = Evd.add sigma evk (Evd.find emap	evk) in
+         let emap' = Evd.remove emap evk in
+         (one,(sigma',emap'))
+       else
+         (evk::one,(sigma,emap))
+    | _ ->
+       fold_constr collrec acc	c
+  in   
+  snd (collrec ([],(sigma,emap)) c)
+
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
   let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
+  let sigma',emap' = push_duplicated_evars sigma' emap' c in
   let change_exist evar =
     let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in
@@ -559,6 +575,7 @@ let rec expansions_of_var env x =
  *)
 
 exception NotUnique
+exception NotUniqueInType of types
 
 type evar_projection = 
 | ProjectVar 
@@ -570,12 +587,13 @@ let rec find_projectable_vars with_evars env sigma y subst =
     if y = y' or expand_var env y = expand_var env y'
     then (idc,(y'=y,(id,ProjectVar)))
     else if with_evars & isEvar y' then
+      (* TODO: infer conditions for being of unifiable types *)
       let (evk,argsv as t) = destEvar y' in
       let evi = Evd.find sigma evk in
       let subst = make_projectable_subst sigma evi argsv in
       let l = find_projectable_vars with_evars env sigma y subst in
       match l with 
-      | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
+      | [id',p] -> (idc,(true,(id,ProjectEvar(t,evi,id',p))))
       | _ -> failwith ""
     else failwith "" in
   let l = map_succeed is_projectable subst in
@@ -596,6 +614,12 @@ let project_with_effects env sigma effects t subst =
   effects := p :: !effects;
   c
 
+let rec find_solution_type evarenv = function
+  | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
+  | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
+  | (id,ProjectEvar _)::l -> find_solution_type evarenv l
+  | [] -> assert false
+
 (* In case the solution to a projection problem requires the instantiation of
  * subsidiary evars, [do_projection_effects] performs them; it
  * also try to instantiate the type of those subsidiary evars if their
@@ -709,7 +733,7 @@ let filter_along f projs v =
  * such that "hyps' |- ?e : T"
  *)
 
-let do_restrict_hyps_virtual evd evk filter =
+let restrict_hyps evd evk filter =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
        - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
@@ -726,15 +750,15 @@ let do_restrict_hyps_virtual evd evk filter =
     let filter,_ = List.fold_right (fun oldb (l,filter) ->
       if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
       oldfilter ([],List.rev filter) in
-    new_evar evd env ~src:(evar_source evk evd)
-      ~filter:filter evi.evar_concl
+    (env,evar_source evk evd,filter,evi.evar_concl)
 
 let do_restrict_hyps evd evk projs =
   let filter = List.map filter_of_projection projs in
   if List.for_all (fun x -> x) filter then
     evd,evk
   else
-    let evd,nc = do_restrict_hyps_virtual evd evk filter in
+    let env,src,filter,ccl = restrict_hyps evd evk filter in
+    let evd,nc = new_evar evd env ~src ~filter ccl in
     let evd = Evd.evar_define evk nc evd in
     let evk',_ = destEvar nc in
     evd,evk'
@@ -854,7 +878,9 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
       let c, p = match sols with
 	| [] -> raise Not_found
 	| [id,p] -> (mkVar id, p)
-	| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+	| (id,p)::_::_ ->
+	    if choose then (mkVar id, p)
+	    else raise (NotUniqueInType(find_solution_type (evar_env evi) sols))
       in
       let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
@@ -862,14 +888,15 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
       c
     with
       | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
-      | NotUnique ->
+      | NotUniqueInType ty ->
 	  if not !progress then raise NotEnoughInformationToProgress;
 	  (* No unique projection but still restrict to where it is possible *)
 	  let ts = expansions_of_var env t in
 	  let test c = isEvar c or List.mem c ts in
 	  let filter = array_map_to_list test argsv in
 	  let args' = filter_along (fun x -> x) filter argsv in
-	  let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
+	  let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in
+	  let evd,evar = new_evar !evdref evarenv ~src ~filter ty in
 	  let evk',_ = destEvar evar in
 	  let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in
 	  evdref := Evd.add_conv_pb pb evd;
@@ -1122,6 +1149,24 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
   let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
   Evd.add_conv_pb pb evd
 
+(* Util *)
+
+let check_instance_type conv_algo env evd ev1 t2 =
+  let t2 = nf_evar (evars_of evd) t2 in
+  if has_undefined_evars evd t2 then
+    (* May contain larger constraints than needed: don't want to
+       commit to an equal solution while only subtyping is requested *)
+    evd
+  else
+    let typ2 = Retyping.get_type_of env (evars_of evd) (refresh_universes t2) in
+    if isEvar typ2 then (* Don't want to commit too early too *) evd
+    else
+      let typ1 = existential_type (evars_of evd) ev1 in
+      let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
+      if b then evd else
+	user_err_loc (fst (evar_source (fst ev1) evd),"",
+	  str "Unable to find a well-typed instantiation")
+
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
@@ -1136,15 +1181,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 	  if evk1 = evk2 then
 	    solve_refl conv_algo env evd evk1 args1 args2
 	  else
-	    if pbty = Reduction.CONV 
+	    if pbty = None
 	    then solve_evar_evar evar_define env evd ev1 ev2
-	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
+	    else if pbty = Some true then
+	      add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
+	    else
+	      add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
       | _ ->
+	  let evd =
+	    if pbty = Some false then
+	      check_instance_type conv_algo env evd ev1 t2 
+	    else
+	      evd in
 	  let evd = evar_define ~choose env ev1 t2 evd in
 	  let evm = evars_of evd in
 	  let evi = Evd.find evm evk1 in
 	    if occur_existential evm evi.evar_concl then
-	      let evenv = evar_env evi in
+	      let evenv = evar_unfiltered_env evi in
 	      let evc = nf_isevar evd evi.evar_concl in
 		match evi.evar_body with 
 		| Evar_defined body -> 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index cb54f400..eef41da3 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
+(*i $Id: evarutil.mli 12268 2009-08-11 09:02:16Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -80,7 +80,7 @@ val solve_refl :
     evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
+  -> ?choose:bool -> env ->  evar_defs -> bool option * existential * constr ->
     evar_defs * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 740b2ca8..f579afa6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacred.ml 12233 2009-07-08 22:50:56Z herbelin $ *)
 
 open Pp
 open Util
@@ -137,20 +137,27 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-(* Check that c is an "elimination constant"
+(* [compute_consteval] determines whether c is an "elimination constant"
 
-   either [xn:An]..[x1:A1](<P>Case (Rel i) of f1..fk end g1 ..gp)
+   either [yn:Tn]..[y1:T1](match yi with f1..fk end g1 ..gp)
 
-   or     [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip))
-          with i1..ip distinct variables not occuring in t 
+   or     [yn:Tn]..[y1:T1](Fix(f|t) yi1..yip)
+          with yi1..yip distinct variables among the yi, not occurring in t 
 
-   In the second case, keep relevenant information ([i1,Ai1;..;ip,Aip],n)
-   in order to compute an equivalent of Fix(f|t)[xi<-ai] as 
+   In the second case, [check_fix_reversibility [T1;...;Tn] args fix] 
+   checks that [args] is a subset of disjoint variables in y1..yn (a necessary
+   condition for reversibility). It also returns the relevant
+   information ([i1,Ti1;..;ip,Tip],n) in order to compute an
+   equivalent of Fix(f|t) such that
 
-      [yip:Bip]..[yi1:Bi1](F bn..b1) 
-   == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel p)..(Rel 1))
+   g := [xp:Tip']..[x1:Ti1'](f a1..an)
+     == [xp:Tip']..[x1:Ti1'](Fix(f|t) yi1..yip)
 
-   with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
+   with a_k:=y_k if k<>i_j, a_k:=args_k otherwise, and 
+   Tij':=Tij[x1..xi(j-1) <- a1..ai(j-1)]
+
+   Note that the types Tk, when no i_j=k, must not be dependent on
+   the xp..x1.
 *)
 
 let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
@@ -172,8 +179,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
          | _ -> 
 	     raise Elimconst) args
   in
-  if not (list_distinct (List.map fst li)) then 
+  let reversible_rels = List.map fst li in
+  if not (list_distinct reversible_rels) then 
     raise Elimconst;
+  list_iter_i (fun i t_i ->
+    if not (List.mem_assoc (i+1) li) then
+      let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
+      if list_intersect fvs reversible_rels <> [] then raise Elimconst)
+    labs;
   let k = lv.(i) in
   if k < nargs then
 (*  Such an optimisation would need eta-expansion 
@@ -294,19 +307,22 @@ let rev_firstn_liftn fn ln =
 (* If f is bound to EliminationFix (n',infos), then n' is the minimal
    number of args for starting the reduction and infos is
    (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts
-   to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where we can remark that
-   yij = Rel(n+1-j)
+   to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where the y_{i_j} consist in a
+   disjoint subset of the yi, i.e. 1 <= ij <= n and the ij are disjoint (in
+   particular, p <= n).
+
+   f is applied to largs := arg1 .. argn and we need for recursive
+   calls to build the function
 
-   f is applied to largs and we need for recursive calls to build the function
       g := [xp:Tip',...,x1:Ti1'](f a1 ... an)
 
    s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up)
 
    This is made possible by setting 
-      a_k:=z_j    if k=i_j
-      a_k:=y_k    otherwise
+      a_k:=x_j    if k=i_j for some j
+      a_k:=arg_k  otherwise
 
-   The type Tij' is Tij[yn..yi(j-1)..y1 <- ai(j-1)..a1]
+   The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1]
 *)
 
 let x = Name (id_of_string "x")
@@ -328,7 +344,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
       | Some (minargs,ref) ->
           let body = applistc (mkEvalRef ref) la in
           let g = 
-            list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
+            list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
               let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
               let tij' = substl (List.rev subst) tij in
 	      mkLambda (x,tij',c)) 1 body (List.rev lv)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bfd601e2..c92f1fc6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
+(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
 
 open Pp
 open Util
@@ -517,7 +517,7 @@ let order_metas metas =
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
 let solve_simple_evar_eqn env evd ev rhs =
-  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
+  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
   if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
   let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
   if not b then error "Cannot solve unification constraints";
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index f8fc4e87..134a4d8b 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
 
 open Names
 open Term
@@ -45,7 +45,7 @@ type split_tree=
   | Split_patt of Idset.t * inductive * 
 		(bool array * (Idset.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * int)
+  | End_patt of (identifier * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
@@ -124,3 +124,4 @@ let get_last env =
   try 
     let (id,_,_) =  List.hd (Environ.named_context env) in id
   with Invalid_argument _ -> error "no previous statement to use"
+
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index 77bee313..bcfd6a96 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: decl_mode.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Names
 open Term
@@ -33,7 +33,7 @@ type split_tree=
   | Split_patt of Idset.t * inductive *
 		(bool array * (Idset.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * int)
+  | End_patt of (identifier * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
diff --git a/proofs/logic.ml b/proofs/logic.ml
index caf6f56b..c019d45f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *)
 
 open Pp
 open Util
@@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
-    try find_mrectype env sigma ct
+    try find_mrectype env sigma (nf_evar sigma ct)
     with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec pj c in
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 784e2d51..69357b2f 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqc.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id: coqc.ml 12911 2010-04-09 10:08:37Z herbelin $ *)
 
 (* Afin de rendre Coq plus portable, ce programme Caml remplace le script
    coqc. 
@@ -126,8 +126,8 @@ let parse_args () =
         parse (cfiles,args) rem
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-    | ("-I"|"-include"|"-outputstate"
-      |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
+    | ("-outputstate"|"-inputstate"|"-is"
+      |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
       |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
 	begin
@@ -135,7 +135,17 @@ let parse_args () =
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
 	    | []        -> usage ()
 	end
-    | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
+    | ("-I"|"-include" as o) :: rem ->
+	begin
+	  match rem with
+	  | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
+	  | s :: "-as" :: [] -> usage ()
+	  | s :: rem' -> parse (cfiles,s::o::args) rem'
+	  | []        -> usage ()
+	end
+    | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
+    | "-R" :: s :: "-as" :: [] -> usage ()
+    | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
 
     | ("-notactics"|"-debug"|"-nolib"
       |"-debugVM"|"-alltransp"|"-VMno"
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 9a7d30b1..ee8ef1d9 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqmktop.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: coqmktop.ml 12874 2010-03-19 23:15:52Z herbelin $ *)
 
 (* coqmktop is a script to link Coq, analogous to ocamlmktop.
    The command line contains options specific to coqmktop, options for the
@@ -277,7 +277,7 @@ let main () =
   (*file for dynlink *)
   let dynlink=
     if not (!opt || !top) then
-      [(print_int 2; tmp_dynlink())]
+      [tmp_dynlink()]
     else
       []
   in
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index c99884c0..62824670 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
 
 open Util
 open Names
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
       if List.length params <> expected then
 	errorlabstrm "suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
-	     (if expected = 0 then str "none" else int expected) ++ 
+	     (if expected = 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
     let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 62a8ddfc..67d1d41a 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Util
 open Pp
@@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 =
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let nek = 
-    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
+    register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info 
       pat_info.pat_pat ek in  
   let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
     tclTHENS (assert_postpone id clause) 
@@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id =
   let hd2 = applist (mkVar fix_id,args@[obj]) in 
     compose_lam rc (whd_beta gls.sigma hd2)
 
+
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
       Close_patt t,_ ->  
@@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | Skip_patt (_,t),skipped::next_objs -> 
 	let args0 = push_arg skipped args in
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
-    | End_patt (id,nhyps),[] -> 
+    | End_patt (id,(nparams,nhyps)),[] -> 
 	begin
 	  match List.assoc id args with
 	      [None,br_args] -> 
-		let metas = 
-		  list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		let all_metas = 
+		  list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		let param_metas,hyp_metas = list_chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
 		    (tacnext 
-		       (applist (mkVar id,List.rev_append br_args metas))) gls
+		       (applist (mkVar id,
+				 List.append param_metas 
+				   (List.rev_append br_args hyp_metas)))) gls
 	    | _ -> anomaly "wrong stack size"
 	end
     | Split_patt (ids,ind,br), casee::next_objs ->
@@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
     | End_patt (_,_) , _ :: _  -> 
 	anomaly "execute_cases : End of branch with garbage left"
 
-
+let understand_my_constr c gls =
+  let env = pf_env gls in
+  let nc = names_of_rel_context env in
+  let rawc = Detyping.detype false [] nc c in
+  let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc ->  map_rawconstr frob rc in
+    Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+
+let set_refine,my_refine =
+let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
+((fun tac -> refine:= tac),
+(fun c gls -> 
+   let oc = understand_my_constr c gls in
+     !refine oc gls))
 
 (* end focus/claim *)
 		
@@ -1361,7 +1377,7 @@ let end_tac et2 gls =
 	  | ET_Case_analysis,EK_dep tree ->
 		 execute_cases Anonymous pi 
 		   (fun c -> tclTHENLIST 
-		      [refine c;
+		      [my_refine c;
 		       clear clauses;
 		       justification assumption])
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
@@ -1382,7 +1398,7 @@ let end_tac et2 gls =
 			     (fun c ->
 				tclTHENLIST 
 				  [clear [fix_id];
-				   refine c;
+				   my_refine c;
 				   clear clauses;
 				   justification assumption])
 			     (initial_instance_stack clauses) 
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 877c8047..5f4a0485 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Refiner
 open Names
@@ -42,20 +42,20 @@ val execute_cases :
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
 val tree_of_pats : 
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree
 
 val add_branch : 
-  identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val append_branch :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   (Names.Idset.t * Decl_mode.split_tree) option ->
   (Names.Idset.t * Decl_mode.split_tree) option
 
 val append_tree :
-  identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+  identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val build_dep_clause :   Term.types Decl_expr.statement list ->
@@ -65,7 +65,7 @@ val build_dep_clause :   Term.types Decl_expr.statement list ->
     Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
 
 val register_dep_subcase :    
-    Names.identifier * int ->
+    Names.identifier * (int * int) ->
     Environ.env ->
     Decl_mode.per_info ->
     Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -115,3 +115,4 @@ val init_tree:
      (Names.Idset.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
 
+val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58a00419..bf199379 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
+(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *)
 
 open Pp
 open Util
@@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) =
   else
     (cty',rels')
 
+(* Like the above, but recurse over all the rels found until there are
+   no more rels to be found *)
+let minimal_free_rels_rec env sigma =
+  let rec minimalrec_free_rels_rec prev_rels (c,cty) =
+    let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
+    let combined_rels = Intset.union prev_rels direct_rels in
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+    in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels)))
+  in minimalrec_free_rels_rec Intset.empty
+
 (* [sig_clausal_form siglen ty]
     
    Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the 
@@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) =
 
    WARNING: No checking is done to make sure that the 
             sigS(or sigT)'s are actually there.
-          - Only homogenious pairs are built i.e. pairs where all the 
+          - Only homogeneous pairs are built i.e. pairs where all the 
    dependencies are of the same sort
 
    [sig_clausal_form] proceed as follows: the default tuple is
@@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	Evd.existential_opt_value (Evd.evars_of !evdref) 
 	(destEvar ev)
       with
-	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+	| Some w ->
+            let w_type = type_of env sigma w in
+            if Evarconv.e_conv env evdref w_type a then
+              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            else
+              error "Cannot solve a unification problem."
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
@@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
  *)
 
 let make_iterated_tuple env sigma dflt (z,zty) =
-  let (zty,rels) = minimal_free_rels env sigma (z,zty) in
+  let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
   let sort_of_zty = get_sort_of env sigma zty in
   let sorted_rels = Sort.list (<) (Intset.elements rels) in
   let (tuple,tuplety) =
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e517453..4ab40acb 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *)
 
 open Term
 open Proof_type
@@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h =
 let h_simple_induction = h_simple_induction_destruct true
 let h_simple_destruct = h_simple_induction_destruct false
 
-let h_induction_destruct isrec ev l =
+let h_induction_destruct ev isrec l =
   abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> 
     List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
-    (induction_destruct ev isrec l)
+    (induction_destruct isrec ev l)
 let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
 let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
 
@@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
 let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
 let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
 (* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 977b602e..af204e77 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
 let rec tclMAP_i n tacfun = function
   | [] -> tclDO n (tacfun None)
   | a::l -> 
-      if n=0 then error "Too much names."
+      if n=0 then error "Too many names."
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
 let remember_first_eq id x = if !x = no_move then x := MoveAfter id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e798f59a..4cbfa6c2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* ================================= *)
 
 let lemInv id c gls =
+  ignore (pf_get_hyp gls id); (* ensure id exists *)
   try
     let clause = mk_clenv_type_of gls c in
     let clause = clenv_constrain_last_binding (mkVar id) clause in
     Clenvtac.res_pf clause ~allow_K:true gls
   with 
+    | NoSuchBinding ->
+	errorlabstrm ""
+	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
 	   (str "Cannot refine current goal with the lemma " ++ 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 322d25e5..ff3f0887 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -108,6 +108,8 @@ let replace_by_meta env sigma = function
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
         *)
       in
+      if occur_meta ty then
+	error "Unable to manage a dependent metavariable of higher-order type.";
       mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
 
 exception NoMeta
@@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       end
 
   | Case (ci,p,cc,v) ->
+      if occur_meta p then
+       error "Unable to manage a metavariable in the return clause of a match.";
       (* bof... *)
       let nbr = Array.length v in
       let v = Array.append [|p;cc|] v in
@@ -380,3 +384,5 @@ let refine (evd,c) gl =
      complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) evd c in
   tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
+
+let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71b50b66..5c891c58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                  match_next_pattern find_next')
               with
                 | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
-            match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
+            match_next_pattern (fun () ->
+	      let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+	      match_pat lmatch hyp pat) ()
 	| Some patv -> 
 	    match b with
 	    | Some body -> 
@@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
                         | PatternMatchingFailure ->
                             match_next_pattern_in_body next_in_body' () in
                     match_next_pattern_in_typ 
-                      (fun () -> match_pat lmeta hyp pat) ()
+                      (fun () ->
+			let hyp = refresh_universes_strict hyp in
+			match_pat lmeta hyp pat) ()
                   with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
                 in
                 match_next_pattern_in_body 
@@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl =
 (***************************************************************************)
 (* Other entry points *)
 
-let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+let glob_tactic x =
+  Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
 
 let glob_tactic_env l env x = 
   Flags.with_option strict_check
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0a8b5d01..0a4c0fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *)
 
 open Pp
 open Util
@@ -249,14 +249,51 @@ let change_option occl t = function
     Some id -> change_in_hyp occl t id
   | None -> change_in_concl occl t
 
-let change occl c cls =
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
+
+let adjust_clause occl cls =
+  (* warn as much as possible on loss of occurrence information *)
   (match cls, occl with
       ({onhyps=(Some(_::_::_)|None)}
       |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
       Some _ ->
 	error "No occurrences expected when changing several hypotheses."
     | _ -> ());
-  onClauses (change_option occl c) cls
+  (* get at clause from cls if only goal or one hyp specified *)
+  let occl,cls = match occl with
+    | None -> None,cls
+    | Some (occs,c) ->
+	if cls.onhyps=Some[] && occs=all_occurrences then
+	  Some (on_snd (List.map out_arg) cls.concl_occs,c),
+	  {cls with concl_occs=all_occurrences_expr}
+	else
+	  match cls.onhyps with
+	  | Some[(occs',id),l] when 
+	      cls.concl_occs=no_occurrences_expr && occs=all_occurrences -> 
+	      Some (on_snd (List.map out_arg) occs',c),
+	      {cls with onhyps=Some[(all_occurrences_expr,id),l]}
+	  | _ ->
+	      occl,cls in
+  (* check if cls has still specified occs *)
+  if cls.onhyps <> None && 
+    List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr)
+    (Option.get cls.onhyps)
+    || cls.concl_occs <> all_occurrences_expr && 
+       cls.concl_occs <> no_occurrences_expr
+  then
+    Flags.if_verbose Pp.msg_warning
+      (if cls.onhyps=Some[] then
+	str "Trailing \"at\" modifier not taken into account."
+      else
+	str "\"at\" modifier in clause \"in\" not taken into account.");
+  (* Anticipate on onClauses which removes concl if not at all occs *)
+  if cls.concl_occs=no_occurrences_expr then cls
+  else {cls with concl_occs=all_occurrences_expr}
+
+let change occl c cls =
+  onClauses (change_option occl c) (adjust_clause occl cls)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,DEFAULTcast)
@@ -1397,10 +1434,6 @@ let quantify lconstr =
    the left of each x1, ...).
 *)
 
-let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
-  | ArgArg x -> x
-
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
@@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl =
 let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl =
   let env = pf_env gl in
   let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+  let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
   let dephyps = List.map (fun (id,_,_) -> id) deps in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 1729695d..d3e7da6a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*)
 
 open Term
 open Hipattern
@@ -20,6 +20,7 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Util
+open Genarg
 
 let assoc_var s ist =
   match List.assoc (Names.id_of_string s) ist.lfun with
@@ -97,18 +98,21 @@ let is_conj ist =
 let flatten_contravariant_conj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then 
 	let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+        let hyp = valueIn (VConstr hyp) in
 	let intros =
 	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args) 
 	  <:tactic< idtac >> in
 	<:tactic<
           let newtyp := $newtyp in
-	  assert newtyp by ($intros; apply id; split; assumption);
-	  clear id
+          let hyp := $hyp in
+          assert newtyp by ($intros; apply hyp; split; assumption);
+          clear hyp
 	>>
       else
 	<:tactic<fail>>
@@ -129,16 +133,19 @@ let is_disj ist =
 let flatten_contravariant_disj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then 
+	let hyp = valueIn (VConstr hyp) in
 	iter_tac (list_map_i (fun i arg ->
 	  let typ = valueIn (VConstr (mkArrow arg c)) in
 	  <:tactic< 
             let typ := $typ in
-	    assert typ by (intro; apply id; constructor $i; assumption)
-	  >>) 1 args) <:tactic< clear id >>
+            let hyp := $hyp in
+            assert typ by (intro; apply hyp; constructor $i; assumption)
+          >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
       else
 	<:tactic<fail>>
   | _ ->
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 06b4e028..f84d8f58 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *)
+(* $Id: FSetDecide.v 13199 2010-06-25 22:36:22Z letouzey $ *)
 
 (**************************************************************)
 (* FSetDecide.v                                               *)
@@ -346,6 +346,19 @@ the above form:
     (** ** Generic Tactics
         We begin by defining a few generic, useful tactics. *)
 
+    (** remove logical hypothesis inter-dependencies (fix #2136). *)
+
+    Ltac no_logical_interdep :=
+      match goal with
+        | H : ?P |- _ =>
+          match type of P with
+            | Prop =>
+              match goal with H' : context [ H ] |- _ => clear dependent H' end
+            | _ => fail
+          end; no_logical_interdep
+        | _ => idtac
+      end.
+
     (** [if t then t1 else t2] executes [t] and, if it does not
         fail, then [t1] will be applied to all subgoals
         produced.  If [t] fails, then [t2] is executed. *)
@@ -405,7 +418,7 @@ the above form:
         propositions of interest. *)
 
     Inductive FSet_elt_Prop : Prop -> Prop :=
-    | eq_Prop : forall (S : Set) (x y : S),
+    | eq_Prop : forall (S : Type) (x y : S),
         FSet_elt_Prop (x = y)
     | eq_elt_prop : forall x y,
         FSet_elt_Prop (E.eq x y)
@@ -660,6 +673,9 @@ the above form:
   Ltac fsetdec :=
     (** We first unfold any occurrences of [iff]. *)
     unfold iff in *;
+    (** We remove dependencies to logical hypothesis. This way,
+        later "clear" will work nicely (see bug #2136) *)
+    no_logical_interdep;
     (** We fold occurrences of [not] because it is better for
         [intros] to leave us with a goal of [~ P] than a goal of
         [False]. *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 3dc6385d..5f18edcd 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
+(*i $Id: Notations.v 12271 2009-08-11 10:29:45Z herbelin $ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
@@ -68,13 +68,13 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
 (** Notations for sigma-types or subsets *)
 
 Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x  |  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x  |  P  & Q }" (at level 0, x at level 99).
 
 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  |  P  & Q }" (at level 0, x at level 99).
 
-Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
 
 Delimit Scope type_scope with type.
 Delimit Scope core_scope with core.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 2d7e2159..48b4568d 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 11741 2009-01-03 14:34:39Z herbelin $ i*)
+(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
 
 Require Import Notations.
 Require Import Logic.
@@ -174,3 +174,20 @@ Tactic Notation "now" tactic(t) := t; easy.
 
 (** A tactic to document or check what is proved at some point of a script *)
 Ltac now_show c := change c.
+
+(** Clear an hypothesis and its dependencies *)
+
+Tactic Notation "clear" "dependent" hyp(h) :=
+ let rec depclear h :=
+  clear h ||
+  match goal with
+   | H : context [ h ] |- _ => depclear H; depclear h
+  end ||
+  fail "hypothesis to clear is used in the conclusion (maybe indirectly)"
+ in depclear h.
+
+(** Revert an hypothesis and its dependencies :
+    this is actually generalize dependent... *)
+
+Tactic Notation "revert" "dependent" hyp(h) :=
+ generalize dependent h.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index a72283d9..c015854e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
+(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*)
 
 Require Import Le Gt Minus Min Bool.
 
@@ -1081,11 +1081,11 @@ Section Map.
 
   (** [flat_map] *)
 
-  Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : 
-    list B :=
+  Definition flat_map (f:A -> list B) :=
+    fix flat_map (l:list A) {struct l} : list B :=
     match l with
       | nil => nil
-      | cons x t => (f x)++(flat_map f t)
+      | cons x t => (f x)++(flat_map t)
     end.
   
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 21f2513f..f01cbbc5 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: BigQ.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*)
 
 Require Import Field Qfield BigN BigZ QSig QMake.
 
@@ -44,6 +44,11 @@ Delimit Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with BigQ.t.
 
+(* Allow nice printing of rational numerals, either as (Qz 1234)
+   or as (Qq 1234 5678) *)
+Arguments Scope BigQ.Qz [bigZ_scope].
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].			     
+			     
 Infix "+" := BigQ.add : bigQ_scope.
 Infix "-" := BigQ.sub : bigQ_scope.
 Notation "- x" := (BigQ.opp x) : bigQ_scope.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 78cf2892..0b6d1cfe 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith_base.v 11301 2008-08-04 19:41:18Z herbelin $ i*)
+(*i $Id: QArith_base.v 13215 2010-06-29 09:31:45Z letouzey $ i*)
 
 Require Export ZArith.
 Require Export ZArithRing.
@@ -157,16 +157,15 @@ Qed.
 
 (** We now consider [Q] seen as a setoid. *)
 
-Definition Q_Setoid : Setoid_Theory Q Qeq.
-Proof.
- split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
-Qed.
+Add Relation Q Qeq
+  reflexivity proved by Qeq_refl
+  symmetry proved by Qeq_sym
+  transitivity proved by Qeq_trans
+as Q_Setoid.
 
-Add Setoid Q Qeq Q_Setoid as Qsetoid.
-
-Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
+Hint Resolve Qeq_refl : qarith.
+Hint Resolve Qeq_sym : qarith.
+Hint Resolve Qeq_trans : qarith.
 
 Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
 Proof.
@@ -633,8 +632,15 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
 Qed.
 
+(** These hints were meant to be added to the qarith database,
+    but a typo prevented that. This will be fixed in 8.3.
+    Concerning 8.2, for maximal compatibility , we
+    leave them in a separate database, in order to preserve
+    the strength of both [auto with qarith] and [auto with *].
+    (see bug #2346). *)
+
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
- Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
+ Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra.
 
 (** Some decidability results about orders. *)
 
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 71befa4a..34771897 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zbool.v 11208 2008-07-04 16:57:46Z letouzey $ *)
+(* $Id: Zbool.v 12271 2009-08-11 10:29:45Z herbelin $ *)
 
 Require Import BinInt.
 Require Import Zeven.
@@ -18,9 +18,9 @@ Require Import Sumbool.
 Unset Boxed Definitions.
 Open Local Scope Z_scope.
 
-(** * Boolean operations from decidabilty of order *)
+(** * Boolean operations from decidability of order *)
 (** The decidability of equality and order relations over
-    type [Z] give some boolean functions with the adequate specification. *)
+    type [Z] gives some boolean functions with the adequate specification. *)
 
 Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y).
 Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y).
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 425aa83b..73808f92 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
+(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*)
 
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
@@ -1025,3 +1025,5 @@ Qed.
 
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
+Notation Zle_gt_succ := Zlt_gt_succ (only parsing).
+Notation Zle_succ_gt := Zlt_succ_gt (only parsing).
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index eb3a19fa..3ca1e7d3 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
+(* $Id: coq_makefile.ml4 12470 2009-11-05 15:50:20Z notin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -163,7 +163,7 @@ let install_include_by_root var files (_,inc_r) =
     let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
     let pdir = physical_dir_of_logical_dir ldir in
     printf "\t(for i in $(%s); do \\\n" var;
-    printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir;
+    printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir;
     printf "\t done)\n"
   with Not_found ->
     (* Files in the scope of a -R option (assuming they are disjoint) *)
@@ -172,12 +172,12 @@ let install_include_by_root var files (_,inc_r) =
 	begin
 	  let pdir' = physical_dir_of_logical_dir ldir in
 	  printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i;
-	  printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir';
+	  printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir';
 	  printf "\t done)\n"
 	end) inc_r;
     (* Files not in the scope of a -R option *)
     printf "\t(for i in $(%s0); do \\\n" var;
-    printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
+    printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
     printf "\t done)\n"
 
 let install (vfiles,mlfiles,_,sds) inc =
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4febe9d1..91a7e6d0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *)
+(* $Id: coqdep.ml 12916 2010-04-10 15:18:17Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -60,7 +60,9 @@ let safe_hash_add clq q (k,v) =
           (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
         | cl::cltl -> cl::add_clash cltl
         | [] -> [(k,[v;v2])] in
-      clq := add_clash !clq
+      clq := add_clash !clq;
+      (* overwrite previous bindings, as coqc does *)
+      Hashtbl.add q k v
   with Not_found -> Hashtbl.add q k v
 
 (* Files found in the loadpaths *)
@@ -167,6 +169,37 @@ let cut_prefix p s =
   let ls = String.length s in
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
+(* Makefile's escaping rules are awful: $ is escaped by doubling and
+   other special characters are escaped by backslash prefixing while
+   backslashes themselves must be escaped only if part of a sequence
+   followed by a special character (i.e. in case of ambiguity with a
+   use of it as escaping character).  Moreover (even if not crucial)
+   it is apparently not possible to directly escape ';' and leading '\t'. *)
+
+let escape =
+  let s' = Buffer.create 10 in
+  fun s ->
+    Buffer.clear s';
+    for i = 0 to String.length s - 1 do
+      let c = s.[i] in
+      if c = ' ' or c = '#' or c = ':' (* separators and comments *)
+	or c = '%' (* pattern *)
+	or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *)
+	or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
+	    'A' <= s.[1] && s.[1] <= 'Z' || 
+	    'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
+      then begin
+	let j = ref (i-1) in
+	while !j >= 0 && s.[!j] = '\\' do 
+	  Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
+	done;
+	Buffer.add_char s' '\\';
+      end;
+      if c = '$' then Buffer.add_char s' '$';
+      Buffer.add_char s' c
+    done;
+    Buffer.contents s'
+
 let canonize f =
   let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
   match List.filter (fun (_,full) -> f' = full) !vAccu with
@@ -423,6 +456,11 @@ let add_coqlib_known phys_dir log_dir f =
     Hashtbl.add coqlibKnown [basename] ();
     Hashtbl.add coqlibKnown name ()
 
+let rec suffixes = function
+  | [] -> assert false
+  | [name] -> [[name]]
+  | dir::suffix as l -> l::suffixes suffix
+
 let add_known phys_dir log_dir f = 
   if (Filename.check_suffix f ".ml" ||  Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4")  then
     let basename = make_ml_module_name f in
@@ -431,7 +469,7 @@ let add_known phys_dir log_dir f =
     let basename = Filename.chop_suffix f ".v" in
     let name = log_dir@[basename] in
     let file = phys_dir//basename in
-    let paths = [name;[basename]] in
+    let paths = suffixes name in
     List.iter
       (fun n -> safe_hash_add clash_v vKnown (n,file)) paths
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c4a1a76f..b29e0734 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -126,7 +126,7 @@
     Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
   let printing_token_re =
     Str.regexp
-      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
 
   let add_printing_token toks pps =
     try
@@ -731,6 +731,9 @@ and body = parse
   | token_no_brackets
       { let s = lexeme lexbuf in
 	  symbol lexbuf s; body lexbuf }
+  | ".."
+      { Output.char '.'; Output.char '.';
+        body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
 	  Output.char c; 
           body lexbuf }
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a75b99c..821a73f7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *)
+(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *)
 
 open Pp
 open Util
@@ -266,16 +266,18 @@ let split_notation_string str =
 
 (* Interpret notations with a recursive component *)
 
-let rec find_pattern xl = function
-  | Break n as x :: l, Break n' :: l' when n=n' -> 
-      find_pattern (x::xl) (l,l')
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let rec find_pattern nt xl = function
+  | Break n as x :: l, Break n' :: l' when n=n' ->
+      find_pattern nt (x::xl) (l,l')
   | Terminal s as x :: l, Terminal s' :: l' when s = s' -> 
-      find_pattern (x::xl) (l,l')
-  | [NonTerminal x], NonTerminal x' :: l' ->
-      (x,x',xl),l'
-  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+      find_pattern nt (x::xl) (l,l')
+  | [], NonTerminal x' :: l' ->
+      (out_nt nt,x',List.rev xl),l'
+  | [], Terminal s :: _ | Terminal s :: _, _ ->
       error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
-  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+  | [], Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | ((SProdList _ | NonTerminal _) :: _ | []), _ -> 
       error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
@@ -283,7 +285,8 @@ let rec find_pattern xl = function
 let rec interp_list_parser hd = function
   | [] -> [], [], List.rev hd
   | NonTerminal id :: tl when id = ldots_var ->
-      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+      let hd = List.rev hd in
+      let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let yl,xl,tl'' = interp_list_parser [] tl' in
       (* We remember each pair of variable denoting a recursive part to *)
       (* remove the second copy of it afterwards *)
@@ -299,6 +302,7 @@ let rec interp_list_parser hd = function
       yl, xl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
+
 (* Find non-terminal tokens of notation *)
 
 let unquote_notation_token s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 176f336b..b54700d3 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
  * camlp4deps will not work for this file unless Makefile system enhanced.
  *)
 
-(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *)
 
 open Util
 open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
         let warn = Flags.is_verbose() in
-        let _,gname = where_in_path ~warn !coq_mlpath_copy s in
+        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a1acd1d6..9d64f983 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *)
 
 open Pp
 open Util
@@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc =
     try
       let (line, bol) = line_of_pos 1 0 0 in
       close_in ic;
-      hov 0
-        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
-         hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
-                str"characters " ++
-                Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
+      hov 0 (* No line break so as to follow emacs error message format *)
+        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+         str", line " ++ int line ++ str", characters " ++
+         Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
       fnl ()
     with e ->
       (close_in ic;
@@ -316,7 +315,7 @@ let parse_to_dot =
 let rec discard_to_dot () =
   try 
     Gram.Entry.parse parse_to_dot top_buffer.tokens
-  with Stdpp.Exc_located(_,Token.Error _) -> 
+  with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> 
     discard_to_dot()
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a0acb52..385afbec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -234,12 +234,8 @@ let dump_universes s =
 (* "Locate" commands *)
 
 let locate_file f =
-  try
-    let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
-    msgnl (str file)
-  with Not_found -> 
-    msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
-		  str"on loadpath"))
+  let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
+  msgnl (str file)
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->