Remove non-DFSG contentsupstream/8.3.pl4+dfsg

41 files changed, 314 insertions, 327 deletions

diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 031b06b5..00000000
--- a/.gitignore
+++ /dev/null
@@ -1,107 +0,0 @@
-*.glob
-*.d
-*.d.raw
-*.vo
-*.cm*
-*.annot
-*.spit
-*.spot
-*.o
-*.a
-*.log
-*.aux
-*.dvi
-*.blg
-*.bbl
-*.idx
-*.ilg
-*.toc
-*.atoc
-*.comidx
-*.comind
-*.erridx
-*.errind
-*.haux
-*.hcomind
-*.herrind
-*.hind
-*.htacind
-*.htoc
-*.ind
-*.lof
-*.stamp
-*.tacidx
-*.tacind
-*.v.tex
-*.v.pdf
-*.v.ps
-*.v.html
-revision
-TAGS
-bin/
-config/Makefile
-config/coq_config.ml
-plugins/dp/dp_zenon.ml
-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/coq_lex.ml
-ide/extract_index.ml
-ide/find_phrase.ml
-ide/highlight.ml
-ide/undo.mli
-ide/utf8_convert.ml
-kernel/byterun/coq_jumptbl.h
-kernel/byterun/dllcoqrun.so
-kernel/copcodes.ml
-scripts/tolink.ml
-states/initial.coq
-test-suite/lia.cache
-test-suite/trace
-theories/Numbers/Natural/BigN/NMake_gen.v
-tools/coqdep_lexer.ml
-tools/coqdoc/cpretty.ml
-tools/coqwc.ml
-tools/gallina_lexer.ml
-toplevel/mltop.optml
-plugins/micromega/csdpcert
-toplevel/mltop.byteml
-coqdoc.sty
-ide/index_urls.txt
-doc/faq/html/
-doc/refman/csdp.cache
-doc/refman/trace
-doc/refman/Reference-Manual.pdf
-doc/refman/Reference-Manual.ps
-doc/refman/cover.html
-doc/refman/styles.hva
-doc/refman/Reference-Manual.html
-doc/common/version.tex
-doc/refman/Reference-Manual.sh
-doc/refman/coqide-queries.eps
-doc/refman/coqide.eps
-doc/refman/euclid.ml
-doc/refman/euclid.mli
-doc/refman/heapsort.ml
-doc/refman/heapsort.mli
-doc/refman/html/
-doc/stdlib/Library.out
-doc/stdlib/Library.pdf
-doc/stdlib/Library.ps
-doc/stdlib/Library.coqdoc.tex
-doc/stdlib/html/
-doc/stdlib/index-body.html
-doc/stdlib/index-list.html
-doc/RecTutorial/RecTutorial.html
-doc/RecTutorial/RecTutorial.pdf
-doc/RecTutorial/RecTutorial.ps
-dev/doc/naming-conventions.pdf
-_build
-plugins/*/*_mod.ml
-myocamlbuild_config.ml
-.DS_Store
-.pc
diff --git a/CHANGES b/CHANGES
index b8a5f9ea..954231f8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,10 +1,36 @@
+Changes from V8.3pl3 to V8.3pl4
+===============================
+
+Bug fixes:
+
+- #2724 (using notations with binders in cases patterns was provoking an anomaly)
+- #2723 (alpha-conversion bug #2723 introduced in r12485-12486)
+- #2732 (anomaly when using the tolerance for writing "f atomic_tac"
+    as a short-hand for "f ltac:(atomic_tac)")
+- #2729 (vm_compute: function used to decompose constructors did not handle let-ins)
+- #2728 (compatibility with camlp5 6.05)
+- #2682 (Fail discard the effects of a successful command)
+- #2703 (Undetected universe inconsistency)
+- #2667 (Coq crashes when "Arguments Scope" has too many parameters)
+- Compilation of coqide under MacOS with gtk >= 2.24.11
+- Coqdoc: Fixing missing newline when using "Proof term."
+
+
 Changes from V8.3pl2 to V8.3pl3
 ===============================
 
+The following (non exhaustive) list of bugs have been fixed:
+
 General
 
 - #2411 (Axiom / Hypothesis / Variable allowed again during proofs)
 - #2603 (verify that all names of an inductive block aren't already used)
+- #1804 (pattern-matching compilation bug with highly nested sigma-types)
+- #2615 (anomaly in inferring pattern-matching return type)
+- #2504 (bug in computing universe of polymorphic inductive types)
+- #2407 (stack overflow in Function)
+- #2181 (unnamed but dependent fields in Classes)
+- bug with modules in virtual machine
 
 Modules
 
@@ -17,6 +43,7 @@ Tactics
 - #2467, #2464 (fixes for fsetdec)
 - Document the "appcontext" variant of "context" that better handles
   partial applications.
+- #2640 (ltac anomaly in expecting a tactic and finding a definition)
 
 Coqide
 
@@ -35,6 +62,12 @@ Extraction
 - Forbid Prop-universe-polymorphism of inductive when extracting
   to ocaml, otherwise things may fail badly (report by S. Glondu).
 
+Coqdoc
+
+- #2606 (bad processing of coq escaped in comments)
+- #2423 (handling of -R in coqdoc)
+- fixing garbage when using some greek letters as identifier names
+
 Changes from V8.3pl1 to V8.3pl2
 ===============================
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 76f81264..c8cb58ae 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -274,7 +274,7 @@ let rec explain_exn = function
 (*      let ctx = Check.get_env() in
       hov 0
         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
-  | Stdpp.Exc_located (loc,exc) ->
+  | Compat.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ explain_exn exc)
diff --git a/configure b/configure
index 8498bd70..16b2a82a 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=8.3pl3
+VERSION=8.3pl4
 VOMAGIC=08300
 STATEMAGIC=58300
 DATE=`LANG=C date +"%B %Y"`
@@ -1085,4 +1085,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 14833 2011-12-19 21:57:30Z notin $
+# $Id: configure 15089 2012-03-26 16:41:59Z notin $
diff --git a/ide/coq.ml b/ide/coq.ml
index 1c6229b4..1a5b9def 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Vernac
 open Vernacexpr
@@ -112,7 +112,7 @@ let is_in_proof_mode () =
     | _ -> true
 
 let user_error_loc l s =
-  raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
+  raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
 
 type printing_state = {
   mutable printing_implicit : bool;
@@ -443,7 +443,7 @@ let interp_and_replace s =
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+  | Compat.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
   | _ -> false
 
@@ -456,7 +456,7 @@ let print_toplevel_error exc =
   in
   let (loc,exc) =
     match exc with
-      | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
+      | Compat.Exc_located (loc, ie) -> (Some loc),ie
       | Error_in_file (s, (_,fname, loc), ie) -> None, ie
       | _ -> dloc,exc
   in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 162728ad..0c99b8a2 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: coqide.ml 15023 2012-03-08 22:35:31Z pboutill $ *)
 
 open Preferences
 open Vernacexpr
@@ -1267,14 +1267,14 @@ object(self)
           | l when List.mem `MOD1 l ->
               let k = GdkEvent.Key.keyval k in
                 if GdkKeysyms._Return=k
-                then ignore(
+                then let _ =
                   if (input_buffer#insert_interactive "\n") then
                     begin
                       let i= self#get_insert#backward_word_start in
                         prerr_endline "active_kp_hf: Placing cursor";
                         self#process_until_iter_or_error i
-                    end);
-                true
+                    end in
+		     true else false
           | l when List.mem `CONTROL l ->
               let k = GdkEvent.Key.keyval k in
                 if GdkKeysyms._Break=k
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4310a01e..96393659 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
+(* $Id: constrintern.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -693,8 +693,9 @@ let apply_scope_env (ids,unb,_,scopes) = function
   | [] -> (ids,unb,None,scopes), []
   | sc::scl -> (ids,unb,sc,scopes), scl
 
-let rec simple_adjust_scopes n = function
-  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+let rec simple_adjust_scopes n scopes =
+  if n=0 then [] else match scopes with
+  | [] -> None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
@@ -771,9 +772,6 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
-let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern.")
-
 let chop_aconstr_constructor loc (ind,k) args =
   if List.length args = 0 then (* Tolerance for a @id notation *) args else
     begin
diff --git a/interp/notation.ml b/interp/notation.ml
index 6e02c40b..4b67f8bd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
+(* $Id: notation.ml 14882 2012-01-05 23:44:40Z herbelin $ *)
 
 (*i*)
 open Util
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2d4e41ec..bcd07aea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: topconstr.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -903,6 +903,12 @@ let names_of_local_binders bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
 
 (**********************************************************************)
+(* Miscellaneous *)
+
+let error_invalid_pattern_notation loc =
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
+
+(**********************************************************************)
 (* Functions on constr_expr *)
 
 let constr_loc = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index ce9de27b..abfbd9a1 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: topconstr.mli 15072 2012-03-20 17:36:33Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -282,3 +282,7 @@ val ntn_loc :
   Util.loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
   Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+
+(** For cases pattern parsing errors *)
+
+val error_invalid_pattern_notation : Util.loc -> 'a
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a97bbe..69828715 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: term.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: term.mli 15029 2012-03-13 14:47:00Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -406,8 +406,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types
 (*s Other term destructors. *)
 
 (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
-   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
-   It includes also local definitions *)
+   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *)
 val decompose_prod : constr -> (name*constr) list * constr
 
 (* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0646a501..869a60e2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: univ.ml 15019 2012-03-02 17:27:18Z letouzey $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -234,48 +234,66 @@ type order = EQ | LT | LE | NLE
 
 (** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
 
-  We try to avoid visiting unneeded parts of this transitive closure,
-  by stopping as soon as [arcv] is encountered. During the recursive
-  traversal, [lt_done] and [le_done] are universes we have already
-  visited, they do not contain [arcv]. The 3rd arg is
-  [(lt_todo,le_todo)], two lists of universes not yet considered,
-  known to be above [arcu], strictly or not.
+  In [strict] mode, we fully distinguish between LE and LT, while in
+  non-strict mode, we simply answer LE for both situations.
+
+  If [arcv] is encountered in a LT part, we could directly answer
+  without visiting unneeded parts of this transitive closure.
+  In [strict] mode, if [arcv] is encountered in a LE part, we could only
+  change the default answer (1st arg [c]) from NLE to LE, since a strict
+  constraint may appear later. During the recursive traversal,
+  [lt_done] and [le_done] are universes we have already visited,
+  they do not contain [arcv]. The 4rd arg is [(lt_todo,le_todo)],
+  two lists of universes not yet considered, known to be above [arcu],
+  strictly or not.
 
   We use depth-first search, but the presence of [arcv] in [new_lt]
   is checked as soon as possible : this seems to be slightly faster
   on a test.
 *)
 
-let compare_neq g arcu arcv =
-  let rec cmp lt_done le_done = function
-  | [],[] -> NLE
+let compare_neq strict g arcu arcv =
+  let rec cmp c lt_done le_done = function
+  | [],[] -> c
   | arc::lt_todo, le_todo ->
     if List.memq arc lt_done then
-      cmp lt_done le_done (lt_todo,le_todo)
+      cmp c lt_done le_done (lt_todo,le_todo)
     else
       let lt_new = can g (arc.lt@arc.le) in
-      if List.memq arcv lt_new then LT
-      else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
+      if List.memq arcv lt_new then
+	if strict then LT else LE
+      else cmp c (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
   | [], arc::le_todo ->
-    if arc == arcv then LE
-    (* No need to continue inspecting universes above arc:
-       if arcv is strictly above arc, then we would have a cycle *)
+    if arc == arcv then
+      (* No need to continue inspecting universes above arc:
+	 if arcv is strictly above arc, then we would have a cycle.
+         But we cannot answer LE yet, a stronger constraint may
+	 come later from [le_todo]. *)
+      if strict then cmp LE lt_done le_done ([],le_todo) else LE
     else
       if (List.memq arc lt_done) || (List.memq arc le_done) then
-	cmp lt_done le_done ([],le_todo)
+	cmp c lt_done le_done ([],le_todo)
       else
 	let lt_new = can g arc.lt in
-	if List.memq arcv lt_new then LT
+	if List.memq arcv lt_new then
+	  if strict then LT else LE
 	else
 	  let le_new = can g arc.le in
-	  cmp lt_done (arc::le_done) (lt_new, le_new@le_todo)
+	  cmp c lt_done (arc::le_done) (lt_new, le_new@le_todo)
   in
-  cmp [] [] ([],[arcu])
+  cmp NLE [] [] ([],[arcu])
 
 let compare g u v =
   let arcu = repr g u
   and arcv = repr g v in
-  if arcu == arcv then EQ else compare_neq g arcu arcv
+  if arcu == arcv then EQ else compare_neq true g arcu arcv
+
+let is_leq g u v =
+  let arcu = repr g u
+  and arcv = repr g v in
+  arcu == arcv || (compare_neq false g arcu arcv = LE)
+
+let is_lt g u v = (compare g u v = LT)
 
 (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
                 compare(u,v) = LT or LE => compare(v,u) = NLE
@@ -312,11 +330,11 @@ let rec check_eq g u v =
 let compare_greater g strict u v =
   let g = declare_univ u g in
   let g = declare_univ v g in
-  if not strict && compare_eq g v Set then true else
-  match compare g v u with
-    | (EQ|LE) -> not strict
-    | LT -> true
-    | NLE -> false
+  if strict then
+    is_lt g v u
+  else
+    compare_eq g v Set || is_leq g v u
+
 (*
 let compare_greater g strict u v =
   let b = compare_greater g strict u v in
@@ -340,9 +358,7 @@ let setlt g u v =
   enter_arc {arcu with lt=v::arcu.lt} g
 
 (* checks that non-redundant *)
-let setlt_if g u v = match compare g u v with
-  | LT -> g
-  | _ -> setlt g u v
+let setlt_if g u v = if is_lt g u v then g else setlt g u v
 
 (* setleq : universe_level -> universe_level -> unit *)
 (* forces u >= v *)
@@ -352,9 +368,7 @@ let setleq g u v =
 
 
 (* checks that non-redundant *)
-let setleq_if g u v = match compare g u v with
-  | NLE -> setleq g u v
-  | _ -> g
+let setleq_if g u v = if is_leq g u v then g else setleq g u v
 
 (* merge : universe_level -> universe_level -> unit *)
 (* we assume  compare(u,v) = LE *)
@@ -398,14 +412,12 @@ let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
 let enforce_univ_leq u v g =
   let g = declare_univ u g in
   let g = declare_univ v g in
-  match compare g u v with
-    | NLE ->
-	(match compare g v u with
-           | LT -> error_inconsistency Le u v
-           | LE -> merge g v u
-           | NLE -> setleq g u v
-           | EQ -> anomaly "Univ.compare")
-    | _ -> g
+  if is_leq g u v then g
+  else match compare g v u with
+    | LT -> error_inconsistency Le u v
+    | LE -> merge g v u
+    | NLE -> setleq g u v
+    | EQ -> anomaly "Univ.compare"
 
 (* enforc_univ_eq : universe_level -> universe_level -> unit *)
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
@@ -432,9 +444,8 @@ let enforce_univ_lt u v g =
     | LE -> setlt g u v
     | EQ -> error_inconsistency Lt u v
     | NLE ->
-	(match compare g v u with
-           | NLE -> setlt g u v
-           | _ -> error_inconsistency Lt u v)
+      if is_leq g v u then error_inconsistency Lt u v
+      else setlt g u v
 
 (* Constraints and sets of consrtaints. *)
 
@@ -452,7 +463,13 @@ let enforce_constraint cst g =
 module Constraint = Set.Make(
   struct
     type t = univ_constraint
-    let compare = Pervasives.compare
+    let compare (u,c,v) (u',c',v') =
+      let i = Pervasives.compare c c' in
+      if i <> 0 then i
+      else
+	let i' = cmp_univ_level u u' in
+	if i' <> 0 then i'
+	else cmp_univ_level v v'
   end)
 
 type constraints = Constraint.t
@@ -557,6 +574,14 @@ let no_upper_constraints u cst =
   | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
   | Max _ -> anomaly "no_upper_constraints"
 
+(* Is u mentionned in v (or equals to v) ? *)
+
+let univ_depends u v =
+  match u, v with
+    | Atom u, Atom v -> u = v
+    | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
+    | _ -> anomaly "univ_depends given a non-atomic 1st arg"
+
 (* Pretty-printing *)
 
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cb6dec1..89b20de3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: univ.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: univ.mli 15019 2012-03-02 17:27:18Z letouzey $ i*)
 
 (* Universes. *)
 
@@ -78,6 +78,10 @@ val subst_large_constraints :
 
 val no_upper_constraints : universe -> constraints -> bool
 
+(** Is u mentionned in v (or equals to v) ? *)
+
+val univ_depends : universe -> universe -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 096320ed..a0264dc7 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -15,6 +15,7 @@ IFDEF OCAML309 THEN DEFINE OCAML308 END
 IFDEF CAMLP5 THEN
 module M = struct
 type loc = Stdpp.location
+exception Exc_located = Ploc.Exc
 let dummy_loc = Stdpp.dummy_loc
 let make_loc = Stdpp.make_loc
 let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
@@ -26,6 +27,7 @@ type lexer = token Token.glexer
 end
 ELSE IFDEF OCAML308 THEN
 module M = struct
+exception Exc_located = Stdpp.Exc_located
 type loc = Token.flocation
 let dummy_loc = Token.dummy_loc
 let make_loc loc = Token.make_loc loc
@@ -45,6 +47,7 @@ type lexer = Token.lexer
 end
 ELSE
 module M = struct
+exception Exc_located = Stdpp.Exc_located
 type loc = int * int
 let dummy_loc = (0,0)
 let make_loc x = x
@@ -59,6 +62,7 @@ END
 END
 
 type loc = M.loc
+exception Exc_located = M.Exc_located
 let dummy_loc = M.dummy_loc
 let make_loc = M.make_loc
 let unloc = M.unloc
diff --git a/library/impargs.ml b/library/impargs.ml
index 1c2b5afe..96209505 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: impargs.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Util
 open Names
@@ -209,11 +209,10 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na b =
-  if all then
-    compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
-  else
-    compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+  let flag = RenamingElsewhereFor envnames_b in
+  if all then compute_and_force_displayed_name_in flag avoid na b
+  else compute_displayed_name_in flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
@@ -221,7 +220,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = find_displayed_name_in all avoid na b in
+	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
@@ -234,7 +233,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na b in
+	let na',avoid = find_displayed_name_in all [] na ([],b) in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
diff --git a/man/coqtop.1 b/man/coqtop.1
index a3b3aac4..3eab597f 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -53,7 +53,7 @@ read state from file
 
 .TP
 .B \-nois
-start with an empty intial state
+start with an empty initial state
 
 .TP
 .BI \-outputstate filename
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index ba965a54..072b09fa 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *)
+(* $Id: egrammar.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -109,11 +109,14 @@ let make_constr_action
   in
   make ([],[],[]) (List.rev pil)
 
+let check_cases_pattern_env loc (env,envlist,hasbinders) =
+  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+
 let make_cases_pattern_action
   (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv) = function
+  let rec make (env,envlist,hasbinders as fullenv) = function
   | [] ->
-      Gramext.action (fun loc -> f loc fullenv)
+      Gramext.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
       Gramext.action (fun _ -> make fullenv tl)
@@ -121,28 +124,37 @@ let make_cases_pattern_action
       (* parse a binding non-terminal *)
     (match typ with
     | ETConstr _ -> (* pattern non-terminal *)
-        Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+        Gramext.action (fun (v:cases_pattern_expr) ->
+          make (v::env, envlist, hasbinders) tl)
     | ETReference ->
         Gramext.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
+	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
     | ETName ->
         Gramext.action (fun (na:name located) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
+	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
     | ETBigint ->
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
     | ETConstrList (_,_) ->
         Gramext.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
-	failwith "Unexpected entry of type cases pattern or other")
+	  make (env, vl :: envlist, hasbinders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gramext.action (fun (v:local_binder list) ->
+	  make (env, envlist, hasbinders) tl)
+    | ETBinderList (false,_) ->
+	Gramext.action (fun (v:local_binder list list) ->
+	  make (env, envlist, true) tl)
+    | (ETPattern | ETOther _) ->
+        anomaly "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
       let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      if b then
+        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
+      else
+        make (env,heads::envlist,hasbinders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],false) (List.rev pil)
 
 let rec make_constr_prod_item assoc from forpat = function
   | GramConstrTerminal tok :: l ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 44ac445d..3ed4d8a7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 14657 2011-11-16 08:46:33Z herbelin $ *)
+(* $Id: ppvernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Names
@@ -781,7 +781,7 @@ let rec pr_vernac = function
       (if i = 1 then mt() else int i ++ str ": ") ++
       pr_raw_tactic tac
       ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
-      with UserError _|Stdpp.Exc_located _ -> mt())
+      with UserError _|Compat.Exc_located _ -> mt())
 
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 0d7a9cfe..2fbe3f44 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: tacextend.ml4 15043 2012-03-18 13:57:01Z herbelin $ *)
 
 open Util
 open Genarg
@@ -131,19 +131,27 @@ let make_one_printing_rule se (pt,e) =
 
 let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
 
-let rec contains_epsilon = function
-  | List0ArgType _ -> true
-  | List1ArgType t -> contains_epsilon t
-  | OptArgType _ -> true
-  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
-  | ExtraArgType("hintbases") -> true
-  | _ -> false
-let is_atomic = function
-  | GramTerminal s :: l when
-      List.for_all (function
-          GramTerminal _ -> false
-	| GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
-	-> [s]
+let rec contains_epsilon loc = function
+  | List0ArgType _ as t ->
+      <:expr< Genarg.in_gen $make_globwit loc t$ [] >>
+  | List1ArgType t' as t ->
+      <:expr< Genarg.in_gen $make_globwit loc t$
+         [out_gen $make_globwit loc t'$ $contains_epsilon loc t'$] >>
+  | OptArgType _ as t ->
+      <:expr< Genarg.in_gen $make_globwit loc t$ None >>
+(*  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2*)
+  | ExtraArgType("hintbases") as t ->
+      <:expr< Genarg.in_gen $make_globwit loc t$ (Some []) >> (* fragile *)
+  | _ -> raise Exit
+
+let is_atomic loc = function
+  | GramTerminal s :: l ->
+     (try
+        let l = List.map (function
+          GramTerminal _ -> raise Exit
+	| GramNonTerminal(_,t,_,_) -> contains_epsilon loc t) l
+        in [<:expr< ($str:s$, $mlexpr_of_list (fun x -> x) l$) >>]
+      with Exit -> [])
   | _ -> []
 
 let declare_tactic loc s cl =
@@ -163,8 +171,8 @@ let declare_tactic loc s cl =
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
   let atomic_tactics =
-    mlexpr_of_list mlexpr_of_string
-      (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
+    mlexpr_of_list (fun x -> x)
+      (List.flatten (List.map (fun (al,_) -> is_atomic loc al) cl)) in
   <:str_item<
     declare
       open Pcoq;
@@ -173,9 +181,9 @@ let declare_tactic loc s cl =
       try
         let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in
         List.iter
-          (fun s -> Tacinterp.add_primitive_tactic s
+          (fun (s,l) -> Tacinterp.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
-                 Tacexpr.TacExtend($default_loc$,s,[]))))
+                 Tacexpr.TacExtend($default_loc$,$se$,l))))
           $atomic_tactics$
       with e -> Pp.pp (Cerrors.explain_exn e);
       Egrammar.extend_tactic_grammar $se$ $gl$;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 83868da9..934bf683 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: recdef.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Term
 open Termops
@@ -51,7 +51,8 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index c82abfc8..04eac3a8 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -872,7 +872,7 @@ Arguments Scope Tint [Int_scope].
 Arguments Scope Tplus [romega_scope romega_scope].
 Arguments Scope Tmult [romega_scope romega_scope].
 Arguments Scope Tminus [romega_scope romega_scope].
-Arguments Scope Topp [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope].
 
 Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d3a63410..80e712e5 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -485,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac =
 	      true
 	  else false
 	with
-	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	| Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+	| Compat.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
 	| e -> false
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 749101f7..4205f517 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *)
+(* $Id: cases.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Util
 open Names
@@ -100,7 +100,7 @@ let rec list_try_compile f = function
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _
-	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+	| Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
 	    list_try_compile f t
 
 let force_name =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index abfef8d4..c2dd9f03 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: clenv.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Pp
 open Util
@@ -146,9 +146,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
-
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 (******************************************************************)
@@ -460,8 +457,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_from_env env sigma n 
-	(c,rename_bound_vars_as_displayed [] t) 
+      let clause = mk_clenv_from_env env sigma n
+	(c,rename_bound_vars_as_displayed [] [] t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 14e72807..fe4354b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: detyping.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Pp
 open Util
@@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
-  let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
   let na',avoid' =
     if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
     else compute_displayed_name_in flag avoid na c in
@@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign =
 	| None -> na,avoid
 	| Some c ->
 	    if b<>None then
-	      compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+	      compute_displayed_let_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c
 	    else
-	      compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+	      compute_displayed_name_in
+                (RenamingElsewhereFor (env,c)) avoid na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6e54c170..fe90941d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: inductiveops.ml 15019 2012-03-02 17:27:18Z letouzey $ *)
 
 open Util
 open Names
@@ -403,21 +403,6 @@ let arity_of_case_predicate env (ind,params) dep k =
 (* Inferring the sort of parameters of a polymorphic inductive type
    knowing the sort of the conclusion *)
 
-(* Check if u (sort of a parameter) appears in the sort of the
-   inductive (is). This is done by trying to enforce u > u' >= is
-   in the empty univ graph. If an inconsistency appears, then
-   is depends on u. *)
-let is_constrained is u =
-  try
-    let u' = fresh_local_univ() in
-    let _ =
-      merge_constraints
-        (enforce_geq u (super u')
-          (enforce_geq u' is Constraint.empty))
-        initial_universes in
-    false
-  with UniverseInconsistency _ -> true
-
 (* Compute the inductive argument types: replace the sorts
    that appear in the type of the inductive by the sort of the
    conclusion, and the other ones by fresh universes. *)
@@ -429,7 +414,9 @@ let rec instantiate_universes env scl is = function
   | (na,None,ty)::sign, Some u::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
       let s =
-        if is_constrained is u then
+	(* Does the sort of parameter [u] appear in (or equal)
+           the sort of inductive [is] ? *)
+        if univ_depends u is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstriained sort: replace by fresh universe *)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 45060511..f133d842 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 (* Created from contents that was formerly in termops.ml and
    nameops.ml, Nov 2009 *)
@@ -223,22 +223,27 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let visibly_occur_id id c =
-  let rec occur c = match kind_of_term c with
+let occur_rel p env id =
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+  let rec occur n c = match kind_of_term c with
     | Const _ | Ind _ | Construct _ | Var _
 	  when shortest_qualid_of_global Idset.empty (global_of_constr c)
 	    = qualid_of_ident id -> raise Occur
-    | _ -> iter_constr occur c
+    | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
   in
-  try occur c; false
+  try occur 1 c; false
   with Occur -> true
     | Not_found -> false (* Happens when a global is not in the env *)
 
-let next_ident_away_for_default_printing t id avoid =
-  let bad id = List.mem id avoid or visibly_occur_id id t in
+let next_ident_away_for_default_printing env_t id avoid =
+  let bad id = List.mem id avoid or visibly_occur_id id env_t in
   next_ident_away_from id bad
 
-let next_name_away_for_default_printing t na avoid =
+let next_name_away_for_default_printing env_t na avoid =
   let id = match na with
   | Name id   -> id
   | Anonymous ->
@@ -246,7 +251,7 @@ let next_name_away_for_default_printing t na avoid =
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
       id_of_string "H" in
-  next_ident_away_for_default_printing t id avoid
+  next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
 (* Displaying terms avoiding bound variables clashes *)
@@ -269,13 +274,13 @@ let next_name_away_for_default_printing t na avoid =
 type renaming_flags =
   | RenamingForCasesPattern
   | RenamingForGoal
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 let next_name_for_display flags =
   match flags with
   | RenamingForCasesPattern -> next_name_away_in_cases_pattern
   | RenamingForGoal -> next_name_away_in_goal
-  | RenamingElsewhereFor t -> next_name_away_for_default_printing t
+  | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let compute_displayed_name_in flags avoid na c =
@@ -297,16 +302,20 @@ let compute_displayed_let_name_in flags avoid na c =
   let fresh_id = next_name_for_display flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed avoid c =
-  let rec rename avoid c =
+let rec rename_bound_vars_as_displayed avoid env c =
+  let rec rename avoid env c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkProd (na', c1, rename avoid' c2)
+	let na',avoid' =
+          compute_displayed_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkProd (na', c1, rename avoid' (add_name na' env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
-	mkLetIn (na',c1,t, rename avoid' c2)
-    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+	let na',avoid' =
+          compute_displayed_let_name_in
+            (RenamingElsewhereFor (env,c2)) avoid na c2 in
+	mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2)
+    | Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
     | _ -> c
   in
-  rename avoid c
+  rename avoid env c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index f99ee3f6..464efcf8 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: namegen.mli 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Names
 open Term
@@ -64,7 +64,7 @@ val next_name_away_with_default : string -> name -> identifier list ->
 type renaming_flags =
   | RenamingForCasesPattern (* avoid only global constructors *)
   | RenamingForGoal (* avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of constr
+  | RenamingElsewhereFor of (name list * constr)
 
 val make_all_name_different : env -> env
 
@@ -74,4 +74,5 @@ val compute_and_force_displayed_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_displayed_let_name_in :
   renaming_flags -> identifier list -> name -> constr -> name * identifier list
-val rename_bound_vars_as_displayed : identifier list -> types -> types
+val rename_bound_vars_as_displayed :
+  identifier list -> name list -> types -> types
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 688a25b9..a9b2a18b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: pretype_errors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Util
 open Stdpp
@@ -45,7 +45,7 @@ exception PretypeError of env * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+  | Compat.Exc_located(_,(Util.UserError _ | TypeError _ |
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 62941a76..7b09f957 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: typeclasses_errors.ml 15025 2012-03-09 14:27:07Z glondu $ i*)
 
 (*i*)
 open Names
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
       raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
   | Some ev ->
       let loc, kind = Evd.evar_source ev evd in
-	raise (Stdpp.Exc_located (loc, TypeClassError
+	raise (Compat.Exc_located (loc, TypeClassError
 	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
@@ -55,5 +55,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan
 let rec unsatisfiable_exception exn =
   match exn with
   | TypeClassError (_, UnsatisfiableConstraints _) -> true
-  | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
+  | Compat.Exc_located(_, e) -> unsatisfiable_exception e
   | _ -> false
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 395f5c8d..57b183d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: vnorm.ml 15029 2012-03-13 14:47:00Z herbelin $ i*)
 
 open Names
 open Declarations
@@ -111,7 +111,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
     let typi = type_constructor mind mib cty params in
-    let decl,indapp = Term.decompose_prod typi in
+    let decl,indapp = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
@@ -195,11 +195,8 @@ and nf_stk env c t stk  =
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
 	let decl,codom = btypes.(i) in
-	let env =
-	  List.fold_right
-	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
-	let b = nf_val env v codom in
-	compose_lam decl b
+	let b = nf_val (push_rel_context decl env) v codom in
+	it_mkLambda_or_LetIn b decl
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index d837dca5..90514992 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: logic.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -48,7 +48,7 @@ exception RefinerError of refiner_error
 open Pretype_errors
 
 let rec catchable_exception = function
-  | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | Compat.Exc_located(_,e) -> catchable_exception e
   | LtacLocated(_,e) -> catchable_exception e
   | Util.UserError _ | TypeError _
   | RefinerError _ | Indrec.RecursionSchemeError _
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a540eef6..87e7f4ce 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: refiner.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -494,15 +494,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
 let catch_failerror e =
   if catchable_exception e then check_for_interrupt ()
   else match e with
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
-  | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
+  | FailError (0,_) | Compat.Exc_located(_, FailError (0,_))
+  | Compat.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
       check_for_interrupt ()
   | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-  | Stdpp.Exc_located(s,FailError (lvl,s')) ->
-      raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
-  | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s')))  ->
+  | Compat.Exc_located(s,FailError (lvl,s')) ->
+      raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
+  | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s')))  ->
       raise
-       (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
+       (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
   | e -> raise e
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 465d1d80..cf9213dd 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: class_tactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -219,7 +219,7 @@ let e_possible_resolve db_list local_db gl =
 
 let rec catchable = function
   | Refiner.FailError _ -> true
-  | Stdpp.Exc_located (_, e) -> catchable e
+  | Compat.Exc_located (_, e) -> catchable e
   | e -> Logic.catchable_exception e
 
 let is_dep gl gls =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c4a2ef44..c7762c69 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: extratactics.ml4 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Pcoq
@@ -580,7 +580,7 @@ let hResolve id c occ t gl =
     try 
       Pretyping.Default.understand sigma env t_hole
     with 
-    | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
+    | Compat.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
         resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index fd3eeeb2..cf5fab0c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1057,7 +1057,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	      else tclIDTAC
 	    in tclTHENLIST [evartac; rewtac] gl
 	  with
-	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+	  | Compat.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
 	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	      Refiner.tclFAIL_lazy 0
 		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6a11384b..929f1013 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 14677 2011-11-17 22:19:38Z herbelin $ *)
+(* $Id: tacinterp.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Constrintern
 open Closure
@@ -93,15 +93,15 @@ let dloc = dummy_loc
 let catch_error call_trace tac g =
   if call_trace = [] then tac g else try tac g with
   | LtacLocated _ as e -> raise e
-  | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
+  | Compat.Exc_located (_,LtacLocated _) as e -> raise e
   | e ->
     let (nrep,loc',c),tail = list_sep_last call_trace in
-    let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
+    let loc,e' = match e with Compat.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
       let loc = if loc = dloc then loc' else loc in
-      raise (Stdpp.Exc_located(loc,e'))
+      raise (Compat.Exc_located(loc,e'))
     else
-      raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+      raise (Compat.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
@@ -1979,14 +1979,14 @@ and eval_with_fail ist is_lazy goal tac =
 	VRTactic (catch_error trace tac goal)
     | a -> a)
   with
-    | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
-    | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
+    | FailError (0,s) | Compat.Exc_located(_, FailError (0,s))
+    | Compat.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
 	raise (Eval_fail (Lazy.force s))
     | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-    | Stdpp.Exc_located(s,FailError (lvl,s')) ->
-	raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
-    | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
-	raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
+    | Compat.Exc_located(s,FailError (lvl,s')) ->
+	raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
+    | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
+	raise (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 63850bd5..a2bcb987 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -309,7 +309,12 @@ let thm_token =
 
 let prf_token =
   "Next" space+ "Obligation"
-  | "Proof" (space* "." | space+ "with")
+  | "Proof" (space* "." | space+ "with" | space+ "using")
+
+let immediate_prf_token =
+  (* Approximation of a proof term, if not in the prf_token case *)
+  (* To be checked after prf_token *)
+  "Proof" space* [^ '.' 'w' 'u']
 
 let def_token =
   "Definition"
@@ -384,7 +389,8 @@ let commands =
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw =
+  immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
 
 let extraction =
   "Extraction"
@@ -607,7 +613,7 @@ and coq = parse
   | prf_token
       { let eol =
 	  if not !Cdglobals.gallina then
-	    begin backtrack lexbuf; body_bol lexbuf end
+	    begin backtrack lexbuf; body lexbuf end
 	  else
 	    let s = lexeme lexbuf in
 	    let eol =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 86057b4b..095f50c6 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: cerrors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -81,7 +81,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Syntax error: Undefined token.")
   | Lexer.Error (Bad_token s) ->
       hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
-  | Stdpp.Exc_located (loc,exc) ->
+  | Compat.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ explain_exn_default_aux anomaly_string report_fn exc)
@@ -156,8 +156,8 @@ let rec process_vernac_interp_error = function
   | Proof_type.LtacLocated (s,exc) ->
       EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
         Some (process_vernac_interp_error exc))
-  | Stdpp.Exc_located (loc,exc) ->
-      Stdpp.Exc_located (loc,process_vernac_interp_error exc)
+  | Compat.Exc_located (loc,exc) ->
+      Compat.Exc_located (loc,process_vernac_interp_error exc)
   | exc ->
       exc
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 9954ff56..551e5574 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: toplevel.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -274,7 +274,7 @@ let set_prompt prompt =
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+  | Compat.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
   | _ -> false
 
@@ -290,7 +290,7 @@ let print_toplevel_error exc =
   in
   let (locstrm,exc) =
     match exc with
-      | Stdpp.Exc_located (loc, ie) ->
+      | Compat.Exc_located (loc, ie) ->
           if valid_buffer_loc top_buffer dloc loc then
             (print_highlight_location top_buffer loc, ie)
           else
@@ -325,7 +325,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 _|Lexer.Error _)) ->
+  with Compat.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
     discard_to_dot()
 
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a7aef93f..de732618 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: vernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 (* Parsing of vernacular. *)
 
@@ -41,14 +41,14 @@ let raise_with_file file exc =
     match re with
       | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
           ((b, f, loc), e)
-      | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
+      | Compat.Exc_located (loc, e) when loc <> dummy_loc ->
           ((false,file, loc), e)
-      | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
+      | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
   in
   raise (Error_in_file (file, inner, disable_drop inex))
 
 let real_error = function
-  | Stdpp.Exc_located (_, e) -> e
+  | Compat.Exc_located (_, e) -> e
   | Error_in_file (_, _, e) -> e
   | e -> e
 
@@ -206,7 +206,9 @@ let rec vernac_com interpfun (loc,com) =
 
     | VernacFail v ->
 	if not !just_parsing then begin try
-	  interp v; raise HasNotFailed
+	  (* If the command actually works, ignore its effects on the state *)
+	  States.with_state_protection
+	    (fun v -> interp v; raise HasNotFailed) v
 	with e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")