From cea92f33654bf924f5be861a946ee5084eca840b Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 23 Feb 2015 18:58:43 +0100
Subject: Fixed 3233 (fresh does not work with a qualid).

fresh now accepts a qualid, and behaves as if given the short name.
Since fresh used to accept an id, supporting qualid is IMO not a new
feature but just a fix. Hence the fix in v8.5.
---
 parsing/g_ltac.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b4d96e5cb1..3cd7dbc9be 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -153,8 +153,12 @@ GEXTEND Gram
       | IDENT "type_term"; c=uconstr -> TacPretype c
       | IDENT "numgoals" -> TacNumgoals ] ]
   ;
+  (* If a qualid is given, use its short name. TODO: have the shortest
+     non ambiguous name where dots are replaced by "_"? Probably too
+     verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ]
+    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
+	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-- 
cgit v1.2.3


From 152d8a93bbb70ca6ad6a7cd629bd508fd16c1a44 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 23 Feb 2015 19:08:08 +0100
Subject: Fixed doc of fresh (was already outdated before fixing #3233).

---
 doc/refman/RefMan-ltac.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index eea53886b8..186bc9add3 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -142,7 +142,7 @@ is understood as
 & | & {\tt idtac} \sequence{\messagetoken}{}\\
 & | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
 & | & {\tt gfail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
-& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
+& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}|~ {\tt fresh} {\qualid}\\
 & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
 & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
 & | & {\tt type of} {\term}\\
@@ -906,8 +906,8 @@ The following expression returns an identifier:
 \end{quote}
 It evaluates to an identifier unbound in the goal. This fresh
 identifier is obtained by concatenating the value of the
-\textrm{\textsl{component}}'s (each of them is, either an {\ident} which
-has to refer to a name, or directly a name denoted by a
+\textrm{\textsl{component}}'s (each of them is, either an {\qualid} which
+has to refer to a (unqualified) name, or directly a name denoted by a
 {\qstring}). If the resulting name is already used, it is padded
 with a number so that it becomes fresh. If no component is
 given, the name is a fresh derivative of the name {\tt H}.
-- 
cgit v1.2.3


From d64b5766aa8de3842edae167ce554c36ff46f947 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 19:48:54 +0100
Subject: Fixing cf6a68b45 on integrating ensure_evar_independent into
 is_constrainable_in.

---
 pretyping/evarsolve.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b01f29a40a..307edcc89a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
+let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
@@ -1025,21 +1025,21 @@ let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false force k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false force k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2
+      Array.for_all (is_constrainable_in false force env evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
+  | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2
   | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
-  | _ -> (* We don't try to be more clever *) true
+  | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
 
-let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t =
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true force k (ev,fvs) t
+  | _ -> is_constrainable_in true force env evd k (ev,fvs) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
@@ -1049,7 +1049,7 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases force k2 evk2 fvs2)
+    (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
-- 
cgit v1.2.3


From ebfc19d792492417b129063fb511aa423e9d9e08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 22:27:53 +0100
Subject: Compensating 6fd763431 on postponing subtyping evar-evar problems.

Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
---
 pretyping/evarsolve.ml          | 12 ++++++------
 pretyping/evd.ml                |  4 +++-
 pretyping/evd.mli               |  2 +-
 test-suite/complexity/bug4076.v | 29 +++++++++++++++++++++++++++++
 4 files changed, 39 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/complexity/bug4076.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 307edcc89a..9f1b118fb3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -121,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
-  | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+  | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+  | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+  | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
@@ -1111,13 +1111,13 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
     with CannotProject (evd,ev2) ->
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9313e22320..4e38bd4e66 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -779,7 +779,9 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+  else {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cf6ba07c60..48704f75bb 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -397,7 +397,7 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
new file mode 100644
index 0000000000..2c87a908f4
--- /dev/null
+++ b/test-suite/complexity/bug4076.v
@@ -0,0 +1,29 @@
+(* Check behavior of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i : nat), P i -> P i.
+Parameter P : nat -> Type.
+
+Definition g (n : nat) (a0 : P n) : P n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  a17.
-- 
cgit v1.2.3


From 061519fe518fc090a727957f7e46cbe67e10c633 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Feb 2015 11:39:34 +0100
Subject: Univs: Fix Check calling the kernel to retype in the wrong
 environment. Fixes bug #4089.

---
 test-suite/bugs/closed/4089.v | 373 ++++++++++++++++++++++++++++++++++++++++++
 toplevel/vernacentries.ml     |   2 +-
 2 files changed, 374 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4089.v

diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
new file mode 100644
index 0000000000..0ccbf5652f
--- /dev/null
+++ b/test-suite/bugs/closed/4089.v
@@ -0,0 +1,373 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Open Scope type_scope.
+
+Global Set Universe Polymorphism.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+
+Ltac rapply p :=
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
+
+Local Unset Elimination Schemes.
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Ltac transitivity x := etransitivity x.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Definition paths_rect := paths_ind.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Local Open Scope path_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : f == g
+  := fun x => match h with idpath => 1 end.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Arguments eisadj {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Bind Scope equiv_scope with Equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ q
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+  := match r with idpath => 1 end.
+Module Export Equivalences.
+
+Generalizable Variables A B C f g.
+
+Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  BuildIsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+
+Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.
+
+Arguments equiv_idmap {A} , A.
+
+Notation "1" := equiv_idmap : equiv_scope.
+
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000
+  := BuildIsEquiv A C (compose g f)
+    (compose f^-1 g^-1)
+    (fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
+    (fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
+    (fun a =>
+      (whiskerL _ (eisadj g (f a))) @
+      (ap_pp g _ _)^ @
+      ap02 g
+      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
+        (ap_compose f^-1 f _ @@ eisadj f a) @
+        (ap_pp f _ _)^
+      ) @
+      (ap_compose f g _)^
+    ).
+
+Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
+  `{IsEquiv B C g} `{IsEquiv A B f}
+  : A <~> C
+  := BuildEquiv A C (compose g f) _.
+
+Global Instance transitive_equiv : Transitive Equiv | 0 :=
+  fun _ _ _ f g => equiv_compose g f.
+
+Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
+admit.
+Defined.
+
+Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.
+
+End Equivalences.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z').
+admit.
+Defined.
+
+Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
+: IsEquiv (path_prod_uncurried z z') | 0.
+admit.
+Defined.
+
+Definition equiv_path_prod {A B : Type} (z z' : A * B)
+  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
+  := BuildEquiv _ _ (path_prod_uncurried z z') _.
+
+Generalizable Variables X A B C f g n.
+
+Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) (g : forall a, P a -> Q (f a))
+: sigT P -> sigT Q
+  := fun u => (f u.1 ; g u.1 u.2).
+
+Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: IsEquiv (functor_sigma f g) | 1000.
+admit.
+Defined.
+
+Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) `{IsEquiv A B f}
+           (g : forall a, P a -> Q (f a))
+           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: sigT P <~> sigT Q
+  := BuildEquiv _ _ (functor_sigma f g) _.
+
+Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
+           (f : A <~> B)
+           (g : forall a, P a <~> Q (f a))
+: sigT P <~> sigT Q
+  := equiv_functor_sigma f g.
+
+Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
+           (g : forall a, P a <~> Q a)
+: sigT P <~> sigT Q
+  := equiv_functor_sigma' 1 g.
+
+Definition Bip : Type := { C : Type &  C * C }.
+
+Definition BipMor (X Y : Bip) : Type :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) =>
+    { f : C -> D & (f c0 = d0) * (f c1 = d1) }
+  end.
+
+Definition bipmor2map {X Y : Bip} : BipMor X Y -> X.1 -> Y.1 :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) => fun i =>
+    match i with (f;_) => f end
+  end.
+
+Definition bipidmor {X : Bip} : BipMor X X :=
+  match X with (C;(c0,c1)) => (idmap; (1, 1)) end.
+
+Definition bipcompmor {X Y Z : Bip} : BipMor X Y -> BipMor Y Z -> BipMor X Z :=
+  match X, Y, Z with (C;(c0,c1)), (D;(d0,d1)), (E;(e0,e1)) => fun i j =>
+    match i, j with (f;(f0,f1)), (g;(g0,g1)) =>
+      (g o f; (ap g f0 @ g0, ap g f1 @ g1))
+    end
+  end.
+
+Definition isbipequiv {X Y : Bip} (i : BipMor X Y) : Type :=
+  { l : BipMor Y X & bipcompmor i l = bipidmor } *
+  { r : BipMor Y X & bipcompmor r i = bipidmor }.
+
+Lemma bipequivEQequiv : forall {X Y : Bip} (i : BipMor X Y),
+  isbipequiv i <~> IsEquiv (bipmor2map i).
+Proof.
+assert (equivcompmor : forall {X Y : Bip} (i : BipMor X Y) j,
+(bipcompmor i j = bipidmor) <~> Unit).
+  intros; set (U := X); set (V := Y); destruct X as [C [c0 c1]], Y as [D [d0 d1]].
+  transitivity { n : (bipcompmor i j).1 = (@bipidmor U).1 &
+  (bipcompmor i j).2 = transport (fun h => (h c0 = c0) * (h c1 = c1)) n^ (@bipidmor U).2}.
+    admit.
+  destruct i as [f [f0 f1]]; destruct j as [g [g0 g1]].
+
+  transitivity { n : g o f = idmap & (ap g f0 @ g0 = apD10 n c0 @ 1) *
+  (ap g f1 @ g1 = apD10 n c1 @ 1)}.
+    apply equiv_functor_sigma_id; intro n.
+    assert (Ggen : forall (h0 h1 : C -> C) (p : h0 = h1) u0 u1 v0 v1,
+    ((u0, u1) = transport (fun h => (h c0 = c0) * (h c1 = c1)) p^ (v0, v1)) <~>
+    (u0 = apD10 p c0 @ v0) * (u1 = apD10 p c1 @ v1)).
+      induction p; intros; simpl; rewrite !concat_1p; apply symmetry.
+      by apply (equiv_path_prod (u0,u1) (v0,v1)).
+    rapply Ggen.
+    pose (@paths C).
+    Check (@paths C).
+    Undo.
+    Check (@paths C). (* Toplevel input, characters 0-17:
+Error: Illegal application:
+The term "@paths" of type "forall A : Type, A -> A -> Type"
+cannot be applied to the term
+ "C" : "Type"
+This term has type "Type@{Top.892}" which should be coercible to
+ "Type@{Top.882}".
+*)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 743cfaccdb..a2d2e3d91c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1501,7 +1501,7 @@ let vernac_check_may_eval redexp glopt rc =
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
   let uctx = Evd.universe_context sigma' in
-  let env = Environ.push_context uctx env in
+  let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
     if Evarutil.has_undefined_evars sigma' c then
-- 
cgit v1.2.3


From def8cafc0ceae48d57a44ae120730ea36cb56b88 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 24 Feb 2015 14:38:49 +0100
Subject: Update the list of phony targets produced by coq_makefile. (Fix for
 bug #4084)

Also make uninstall_me.sh a real target with proper dependencies.
---
 tools/coq_makefile.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5213d38e71..b84d15d62e 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -297,7 +297,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && ";
       printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
     in
-    print "uninstall_me.sh:\n";
+    printf "uninstall_me.sh: %s\n" !makefile_name;
     print "\techo '#!/bin/sh' > $@ \n";
     if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
     uninstall_by_root where_what_oth;
@@ -701,9 +701,12 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
   main_targets vfiles mlfiles other_targets inc;
     print ".PHONY: ";
     print_list " "
-      ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" ::
-	  "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" ::
-	  "html" :: "validate" ::
+      ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" ::
+	  "gallina" :: "gallinahtml" :: "html" ::
+	  "install" :: "install-doc" :: "install-natdynlink" :: "install-toploop" ::
+	  "opt" :: "printenv" :: "quick" ::
+	  "uninstall" :: "userinstall" ::
+	  "validate" :: "vio2vo" ::
 	    (sds@(CList.map_filter
 		    (fun (n,_,is_phony,_) ->
 		     if is_phony then Some n else None) sps)));
-- 
cgit v1.2.3


From 2734891ab7e90c5b488416d11c3dc41c224773e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Feb 2015 14:22:02 +0100
Subject: Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on
 integrating ensure_evar_independent into is_constrainable_in.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f1b118fb3..13c63e9784 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1027,7 +1027,7 @@ let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
       let params = fst (Array.chop n args) in
       Array.for_all (is_constrainable_in false force env evd k g) params
   | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2
+  | Prod (na,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force (push_rel (na,None,t1) env) evd k g t2
   | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-- 
cgit v1.2.3


From 9ba579bb98ac8e8964a9baea376ce0c9a89f2615 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 09:59:32 +0100
Subject: CHANGES: Info command + info_auto currently broken.

---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGES b/CHANGES
index 19da2a4c81..712a8a7e92 100644
--- a/CHANGES
+++ b/CHANGES
@@ -260,6 +260,12 @@ Tactics
     an inductive type with indices is fixed
   - residual local definitions are now correctly removed.
 - The rename tactic may now replace variables in parallel.
+- A new "Info" command replaces the "info" tactical discontinued in
+  v8.4. It still gives informative results in many cases.
+- The "info_auto" tactic is known to be broken and does not print a
+  trace anymore. Use "Info 1 auto" instead. The same goes for
+  "info_trivial". On the other hand "info_eauto" still works fine,
+  while "Info 1 eauto" prints a trivial trace.
 
 Program
 
-- 
cgit v1.2.3


From ebf4d8e58eeddaf5237447a9a0f21de48e72caa5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 11:23:03 +0100
Subject: [info] tactical warning: do not suggest [info_auto] and
 [info_trivial].

Since they don't work anymore.
---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3b497faab5..e4558481bc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-	   strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto.");
+	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
-- 
cgit v1.2.3


From 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 11:28:19 +0100
Subject: [info_auto] & [info_trivial]: warning message to help users find
 [Info].

---
 tactics/tacinterp.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e4558481bc..af541b8b9e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1973,6 +1973,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 trivial\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1984,6 +1990,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
   | TacAuto (debug,n,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_auto\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 auto\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-- 
cgit v1.2.3


From 2f41d8e976621b907925546a192e90e60f0e580b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 16:35:42 +0100
Subject: Refactoring in [Constr].

[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
---
 kernel/constr.ml     | 58 +++++++++++++++-------------------------------------
 kernel/constr.mli    |  9 ++++----
 library/universes.ml |  4 ++--
 3 files changed, 22 insertions(+), 49 deletions(-)

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49f748412a..499f196b79 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -464,55 +464,18 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances and [s] to compare sorts; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let compare_head_gen eq_universes eq_sorts f t1 t2 =
-  match kind t1, kind t2 with
-  | Rel n1, Rel n2 -> Int.equal n1 n2
-  | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Id.equal id1 id2
-  | Sort s1, Sort s2 -> eq_sorts s1 s2
-  | Cast (c1,_,_), _ -> f c1 t2
-  | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
-  | App (Cast(c1, _, _),l1), _ -> f (mkApp (c1,l1)) t2
-  | _, App (Cast (c2, _, _),l2) -> f t1 (mkApp (c2,l2))
-  | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      f c1 c2 && Array.equal f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
-  | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
-  | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
-  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
-  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | _ -> false
 
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
-
-(* [compare_head_gen_leq u s sl eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
+(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
    [u] to compare universe instances and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
    not taken into account *)
 
-let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
   match kind t1, kind t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
+  | Var id1, Var id2 -> Id.equal id1 id2
   | Sort s1, Sort s2 -> leq_sorts s1 s2
   | Cast (c1,_,_), _ -> leq c1 t2
   | _, Cast (c2,_,_) -> leq t1 c2
@@ -538,6 +501,17 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
       Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
   | _ -> false
 
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
+   instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
+
+let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
+
 (*******************************)
 (*  alpha conversion functions *)
 (*******************************)
@@ -570,7 +544,7 @@ let leq_constr_univs univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
       compare_leq m n
 
@@ -620,7 +594,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 5d11511b4d..622b33c71f 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -285,15 +285,14 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
-(** [compare_head_gen_leq u s sle f fle c1 c2] compare [c1] and [c2]
-    using [f] to compare the immediate subterms of [c1] of [c2] for
+(** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
+    [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
     instances (the first boolean tells if they belong to a constant),
-    [s] to compare sorts for equality and [sle] for subtyping; Cast's,
-    binders name and Cases annotations are not taken into account *)
+    [s] to compare sorts for for subtyping; Cast's, binders name and
+    Cases annotations are not taken into account *)
 
 val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
-  (Sorts.t -> Sorts.t -> bool) ->
   (Sorts.t -> Sorts.t -> bool) ->
   (constr -> constr -> bool) ->
   (constr -> constr -> bool) ->
diff --git a/library/universes.ml b/library/universes.ml
index 79070763ec..51c2b4d851 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -165,7 +165,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts 
+      Constr.compare_head_gen_leq eq_universes leq_sorts 
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
@@ -213,7 +213,7 @@ let leq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
-- 
cgit v1.2.3


From fc6d0fb650f57a764af6fe9be44677a69be11980 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 16:41:51 +0100
Subject: New function [Constr.equal_with] to compare terms up to variants of
 [kind_of_term].

To be able to write equality up to evar instantiation instantiation.

Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
---
 kernel/constr.ml  | 43 ++++++++++++++++++++++++++++++++-----------
 kernel/constr.mli |  8 ++++++++
 lib/cArray.ml     | 28 ++++++++++++++++------------
 lib/cArray.mli    |  5 +++++
 4 files changed, 61 insertions(+), 23 deletions(-)

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 499f196b79..e823c01b17 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -464,15 +464,19 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-
-(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
-   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
-   [u] to compare universe instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and
+   [c2] (using [k1] to expose the structure of [c1] and [k2] to expose
+   the structure [c2]) using [eq] to compare the immediate subterms of
+   [c1] of [c2] for conversion if needed, [leq] for cumulativity, [u]
+   to compare universe instances, and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account. Note that as [kind1] and [kind2] are
+   potentially different, we cannot use, in recursive case, the
+   optimisation that physically equal arrays are equals (hence the
+   calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
-  match kind t1, kind t2 with
+let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+  match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
@@ -485,8 +489,8 @@ let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      eq c1 c2 && Array.equal eq l1 l2
+      Int.equal (Array.length l1) (Array.length l2) &&
+        eq c1 c2 && Array.equal_norefl eq l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
@@ -496,11 +500,20 @@ let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
       eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
       Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | _ -> false
 
+(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
+   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
+   [u] to compare universe instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
+  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+
 (* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
    instances and [s] to compare sorts; Cast's,
@@ -523,6 +536,14 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
+let rec equal_with kind1 kind2 m n =
+  (* note that pointer equality is not sufficient to ensure equality
+     up to [eq_evars], because we may evaluates evars of [m] and [n]
+     in different evar contexts. *)
+  let req_constr m n = equal_with kind1 kind2 m n in
+  compare_head_gen_with kind1 kind2
+    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
+
 let eq_constr_univs univs m n =
   if m == n then true
   else 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 622b33c71f..67d1adedf6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,6 +203,14 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
+(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
+    alpha, casts, application grouping, and using [k1] to expose the
+    head of [a] and [k2] to expose the head of [b]. *)
+val equal_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  constr -> constr -> bool
+
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 1603454304..bb1e335468 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -13,6 +13,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   val is_empty : 'a array -> bool
   val exists : ('a -> bool) -> 'a array -> bool
   val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -85,19 +86,22 @@ let compare cmp v1 v2 =
       in
       loop (len - 1)
 
+let equal_norefl cmp t1 t2 =
+  let len = Array.length t1 in
+  if not (Int.equal len (Array.length t2)) then false
+  else
+    let rec aux i =
+      if i < 0 then true
+      else
+        let x = uget t1 i in
+        let y = uget t2 i in
+        cmp x y && aux (pred i)
+    in
+    aux (len - 1)
+
 let equal cmp t1 t2 =
-  if t1 == t2 then true else
-    let len = Array.length t1 in
-    if not (Int.equal len (Array.length t2)) then false
-    else
-      let rec aux i =
-        if i < 0 then true
-        else
-          let x = uget t1 i in
-          let y = uget t2 i in
-          cmp x y && aux (pred i)
-      in
-      aux (len - 1)
+  if t1 == t2 then true else equal_norefl cmp t1 t2
+    
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 39c35e2d54..7e5c93b5da 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -17,6 +17,11 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   (** Lift equality to array type. *)
 
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Like {!equal} but does not assume that equality is reflexive: no
+      optimisation is performed if both arrays are physically the
+      same. *)
+
   val is_empty : 'a array -> bool
   (** True whenever the array is empty. *)
 
-- 
cgit v1.2.3


From f7b29094fe7cc13ea475447bd30d9a8b942f0fef Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 12:08:51 +0100
Subject: [Proofview.tclPROGRESS]: do not consider that trivial goal
 instantiation is progress.

Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.

Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).

Fixes bugs (one reported directly on coqdev, and #3412).
---
 pretyping/evarutil.ml  |  5 ++++
 pretyping/evarutil.mli |  7 ++++++
 pretyping/evd.ml       | 29 ----------------------
 pretyping/evd.mli      |  7 ------
 proofs/proofview.ml    | 66 ++++++++++++++++++++++++++++++++++++++++++++------
 5 files changed, 70 insertions(+), 44 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d286b98e83..0b8cbff36c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -838,3 +838,8 @@ let subterm_source evk (loc,k) =
     | Evar_kinds.SubEvar (evk) -> evk
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to isntantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (Reductionops.whd_evar sigma t)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f89266a60a..92a3984ba6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 exception Uninstantiated_evar of existential_key
 val flush_and_check_evars :  evar_map -> constr -> constr
 
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+    value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4e38bd4e66..454c51195b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -568,14 +568,6 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-(* HH: The progress tactical now uses this function. *)
-let progress_evar_map d1 d2 =
-  let is_new k v =
-    assert (v.evar_body == Evar_empty);
-    EvMap.mem k d2.defn_evars
-  in
-  not (d1 == d2) && EvMap.exists is_new d1.undf_evars
-
 let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
   let id = match naming with
   | Misctypes.IntroAnonymous ->
@@ -1303,27 +1295,6 @@ let e_eq_constr_univs evdref t u =
 let eq_constr_univs_test evd t u =
   snd (eq_constr_univs evd t u)
 
-let eq_named_context_val d ctx1 ctx2 = 
-  ctx1 == ctx2 ||
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 
-      && (eq_constr_univs_test d) t1 t2
-    in List.equal eq_named_declaration c1 c2
-
-let eq_evar_body d b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
-| _ -> false
-
-let eq_evar_info d ei1 ei2 =
-  ei1 == ei2 ||
-    eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
-    eq_evar_body d ei1.evar_body ei2.evar_body
-    (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 48704f75bb..0765b951fd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -126,10 +126,6 @@ type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
 
-val progress_evar_map : evar_map -> evar_map -> bool
-(** Assuming that the second map extends the first one, this says if
-   some existing evar has been refined *)
-
 val empty : evar_map
 (** The empty evar map. *)
 
@@ -204,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
 val undefined_map : evar_map -> evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
-(** Compare the evar_info's up to the universe constraints of the evar map. *)
-
 val drop_all_defined : evar_map -> evar_map
 
 (** {6 Instantiating partial terms} *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b6861fd499..6f62634133 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -719,22 +719,72 @@ let give_up =
 
 (** {7 Control primitives} *)
 
-(** Equality function on goals *)
-let goal_equal evars1 gl1 evars2 gl2 =
-  let evi1 = Evd.find evars1 gl1 in
-  let evi2 = Evd.find evars2 gl2 in
-  Evd.eq_evar_info evars2 evi1 evi2
+
+module Progress = struct
+
+  (** equality function up to evar instantiation in heterogeneous
+      contexts. *)
+  (* spiwack (2015-02-19): In the previous version of progress an
+     equality which considers two universes equal when it is consistent
+     tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
+     behaviour has to be restored as well. This has to be established by
+     practice. *)
+    
+  let rec eq_constr sigma1 sigma2 t1 t2 =
+    Constr.equal_with
+      (fun t -> Evarutil.kind_of_term_upto sigma1 t)
+      (fun t -> Evarutil.kind_of_term_upto sigma2 t)
+      t1 t2
+
+  (** equality function on hypothesis contexts *)
+  let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
+    let open Environ in
+    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
+      && (eq_constr sigma1 sigma2) t1 t2
+    in List.equal eq_named_declaration c1 c2
+
+  let eq_evar_body sigma1 sigma2 b1 b2 =
+    let open Evd in
+    match b1, b2 with
+    | Evar_empty, Evar_empty -> true
+    | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
+    | _ -> false
+
+  let eq_evar_info sigma1 sigma2 ei1 ei2 =
+    let open Evd in
+    eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
+    eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
+    eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
+
+  (** Equality function on goals *)
+  let goal_equal evars1 gl1 evars2 gl2 =
+    let evi1 = Evd.find evars1 gl1 in
+    let evi2 = Evd.find evars2 gl2 in
+    eq_evar_info evars1 evars2 evi1 evi2
+
+end
 
 let tclPROGRESS t =
   let open Proof in
   Pv.get >>= fun initial ->
   t >>= fun res ->
   Pv.get >>= fun final ->
+  (* [*_test] test absence of progress. [quick_test] is approximate
+     whereas [exhaustive_test] is complete. *)
+  let quick_test =
+    initial.solution == final.solution && initial.comb == final.comb
+  in
+  let exhaustive_test =
+    Util.List.for_all2eq begin fun i f ->
+      Progress.goal_equal initial.solution i final.solution f
+    end initial.comb final.comb
+  in
   let test =
-    Evd.progress_evar_map initial.solution final.solution &&
-    not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb)
+    quick_test || exhaustive_test
   in
-  if test then
+  if not test then
     tclUNIT res
   else
     tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
-- 
cgit v1.2.3


From 152f57925a6dc08ce3f332319b50eae9fb7bb622 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Feb 2015 18:44:20 +0100
Subject: Calling coq references lazily in plugin cc so as to support static
 linking of plugins.

---
 plugins/cc/cctac.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7110e5b232..8884aef1cf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,7 +23,7 @@ open Pp
 open Errors
 open Util
 
-let reference dir s = Coqlib.gen_reference "CC" dir s
+let reference dir s = lazy (Coqlib.gen_reference "CC" dir s)
 
 let _f_equal = reference ["Init";"Logic"] "f_equal"
 let _eq_rect = reference ["Init";"Logic"] "eq_rect"
@@ -91,7 +91,7 @@ let atom_of_constr env sigma term =
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -126,7 +126,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if is_global _eq f && Int.equal (Array.length args) 3
+	if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -147,7 +147,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -159,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if is_global _False ff then
+	if is_global (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -246,10 +246,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 let _M =mkMeta
 
 let app_global f args k = 
-  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k = 
-  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
@@ -375,9 +375,9 @@ let discriminate_tac (cstr,u as cstru) p =
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
-    let identity = Universes.constr_of_global _I in
+    let identity = Universes.constr_of_global (Lazy.force _I) in
     (* let trivial=pf_type_of gls identity in *)
-    let trivial = Universes.constr_of_global _True in
+    let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
@@ -493,7 +493,7 @@ let f_equal =
     in
     Proofview.tclORELSE
       begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
+      | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r ->
 	  begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
-- 
cgit v1.2.3


From 5a7a90e6fc067319e66c8021e696df98883223f0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 08:11:14 +0100
Subject: An optimization on filtering evar instances with let-ins suggested by
 inefficiency #4076.

In an evar context like this one

x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z)

with unification problem

a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c)

we now keep y after filtering, iff the name b occurs effectively in
v(a,b,c), while before, we kept it as soon as its expansion f(t(a))
had free variables in v(a,b,c), which was more often, but useless
since the point in keeping a let-in in the instance is precisely to
reuse the name of the let-in while unifying with a right-hand side
which mentions this name.
---
 pretyping/evarsolve.ml | 35 ++++++++++++++++++++++++++---------
 1 file changed, 26 insertions(+), 9 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 13c63e9784..a03b50b72d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -315,6 +315,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+  let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
     | Rel n -> Int.Set.mem (n-depth) !cache_rel
@@ -329,8 +330,13 @@ let free_vars_and_rels_up_alias_expansion aliases c =
     | Rel _ | Var _ as ck ->
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c = expansion_of_var aliases c in
+      let c' = expansion_of_var aliases c in
+      (if c != c' then (* expansion, hence a let-in *)
         match kind_of_term c with
+        | Var id -> acc4 := Id.Set.add id !acc4
+        | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
+        | _ -> ());
+      match kind_of_term c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
@@ -342,7 +348,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
           frec (aliases,depth) c
   in
   frec (aliases,0) c;
-  (!acc1,!acc2)
+  (!acc1,!acc2,!acc3,!acc4)
 
 (********************************)
 (* Managing pattern-unification *)
@@ -378,7 +384,7 @@ let get_actual_deps aliases l t =
     l
   else
     (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
     List.filter (fun c ->
       match kind_of_term c with
       | Var id -> Id.Set.mem id fv_ids
@@ -1034,12 +1040,23 @@ let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
 
-let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids as fvs) t =
-  let t = expansion_of_var aliases t in
-  match kind_of_term t with
-  | Var id -> Id.Set.mem id fv_ids
-  | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true force env evd k (ev,fvs) t
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
+  let t' = expansion_of_var aliases t in
+  if t' != t then
+    (* t is a local definition, we keep it only if appears in the list *)
+    (* of let-in variables effectively occurring on the right-hand side, *)
+    (* which is the only reason to keep it when inverting arguments *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id let_ids
+    | Rel n -> Int.Set.mem n let_rels
+    | _ -> assert false
+  else
+    (* t is an instance for a proper variable; we filter it along *)
+    (* the free variables allowed to occur *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id fv_ids
+    | Rel n -> n <= k || Int.Set.mem n fv_rels
+    | _ -> is_constrainable_in true force env evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
-- 
cgit v1.2.3


From 1303e5683cb26f9dd8ed385df08d6a68b6b28fdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 07:40:11 +0100
Subject: Optimizing noccur_evar wrt expansion of let-ins (fix for variant of
 #4076).

---
 pretyping/evarsolve.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a03b50b72d..d3ab4683d8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -178,7 +178,9 @@ let restrict_instance evd evk filter argsv =
   Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
 let noccur_evar env evd evk c =
-  let rec occur_rec k c = match kind_of_term c with
+  let cache = ref Int.Set.empty (* cache for let-ins *) in
+  let rec occur_rec k c =
+  match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
        | Some c -> occur_rec k c
@@ -186,9 +188,10 @@ let noccur_evar env evd evk c =
            if Evar.equal evk evk' then raise Occur
            else Array.iter (occur_rec k) args')
   | Rel i when i > k ->
+      if not (Int.Set.mem (i-k) !cache) then
       (match pi2 (Environ.lookup_rel (i-k) env) with
        | None -> ()
-       | Some b -> occur_rec k (lift i b))
+       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b))
   | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
   | _ -> iter_constr_with_binders succ occur_rec k c
   in
-- 
cgit v1.2.3


From 30406ca1162631ea7e0378dd8b9b3ef437c5d95d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 13:21:52 +0100
Subject: Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integrating
 ensure_evar_independent into is_constrainable_in (a simpler approach closest
 to what existed before cf6a68b45).

---
 pretyping/evarsolve.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index d3ab4683d8..f355d9a725 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1026,22 +1026,24 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args = decompose_app_vect t in
+let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+  let f,args2 = decompose_app_vect t in
+  let f,args1 = decompose_app_vect (whd_evar evd f) in
+  let args = Array.append args1 args2 in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false force env evd k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
-  | Prod (na,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force (push_rel (na,None,t1) env) evd k g t2
-  | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+  | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
+  | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
-  | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
+  | _ -> (* We don't try to be more clever *) true
 
 let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
   let t' = expansion_of_var aliases t in
@@ -1059,7 +1061,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r
     match kind_of_term t with
     | Var id -> Id.Set.mem id fv_ids
     | Rel n -> n <= k || Int.Set.mem n fv_rels
-    | _ -> is_constrainable_in true force env evd k (ev,(fv_rels,fv_ids)) t
+    | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
-- 
cgit v1.2.3


From d1cbd0b21dd73e2b4af3ced394b51877afde40b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 14:00:33 +0100
Subject: Another test for a variant of complexity problem #4076 (thanks to A.
 Mortberg).

---
 test-suite/complexity/bug4076bis.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/complexity/bug4076bis.v

diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
new file mode 100644
index 0000000000..9303e60a21
--- /dev/null
+++ b/test-suite/complexity/bug4076bis.v
@@ -0,0 +1,31 @@
+(* Another check of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i j : nat), P i j -> P i j.
+Parameter P : nat -> nat -> Type.
+
+Timeout 10 Definition g (n : nat) (a0 : P n n) : P n n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  let a18 := f a17 in
+  let a19 := f a18 in
+  a19.
-- 
cgit v1.2.3


From 09fcaf0c38580cc1cb279974517e2ea77c982da3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 25 Feb 2015 15:30:16 +0100
Subject: Reorder the steps of the easy tactic. (Fix for bug #2630)

Due to the way it was laid out, the tactic could prove neither
  (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True)
yet it could prove
  (Zle x x /\ True) and (P /\ Q |- P).
---
 theories/Init/Tactics.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9e828e6ea0..a7d3f8062a 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -180,12 +180,14 @@ Ltac easy :=
     | H : _ |- _ => solve [inversion H]
     | _ => idtac
     end in
-  let rec do_atom :=
-    solve [reflexivity | symmetry; trivial] ||
-    contradiction ||
-    (split; do_atom)
-  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
-  (use_hyps; do_ccl) || fail "Cannot solve this goal".
+  let do_atom :=
+    solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ] in
+  let rec do_ccl :=
+    try do_atom;
+    repeat (do_intro; try do_atom);
+    solve [ split; do_ccl ] in
+  solve [ do_atom | use_hyps; do_ccl ] ||
+  fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.
 
-- 
cgit v1.2.3


From 6900909e90dfa65d1c42bfcd67135e91317a8b2c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 25 Feb 2015 15:31:10 +0100
Subject: Fix phony targets. (Fix for bug #4083)

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index c7fb1ff768..554718bc77 100644
--- a/Makefile
+++ b/Makefile
@@ -169,7 +169,7 @@ Makefile Makefile.build Makefile.common config/Makefile : ;
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean doclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
 
 clean: objclean cruftclean depclean docclean devdocclean
 
-- 
cgit v1.2.3


From 3a291d75ad2d4836d7c62792771f9c9b5f980412 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 25 Feb 2015 16:03:46 +0100
Subject: Not building the doc by default.

Should make the compilation of Coq more robust against LaTeX errors.
See e.g. #4091.
---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 6d30b28312..8667a53594 100644
--- a/configure.ml
+++ b/configure.ml
@@ -245,7 +245,7 @@ module Prefs = struct
   let coqide = ref (None : ide option)
   let macintegration = ref true
   let browser = ref (None : string option)
-  let withdoc = ref true
+  let withdoc = ref false
   let geoproof = ref false
   let byteonly = ref false
   let debug = ref false
-- 
cgit v1.2.3


From f17fa1daa613a4f86e6bdbf51ed7e758f158f938 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Feb 2015 16:25:20 +0100
Subject: STM: proof state also includes meta counters

Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
---
 library/states.ml      |  1 +
 library/states.mli     |  1 +
 pretyping/evarutil.ml  |  8 ++++++--
 pretyping/evarutil.mli |  3 +++
 stm/stm.ml             | 36 ++++++++++++++++++++++++++++--------
 5 files changed, 39 insertions(+), 10 deletions(-)

diff --git a/library/states.ml b/library/states.ml
index a1c2a095d0..96a487b160 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,6 +12,7 @@ open System
 type state = Lib.frozen * Summary.frozen
 
 let summary_of_state = snd
+let replace_summary (lib,_) s = lib, s
 
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
diff --git a/library/states.mli b/library/states.mli
index 66de14909a..4d5d63e037 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
 val summary_of_state : state -> Summary.frozen
+val replace_summary : state -> Summary.frozen -> state
 
 (** {6 Rollback } *)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0b8cbff36c..201a16ebeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 92a3984ba6..49036798e6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -243,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
diff --git a/stm/stm.ml b/stm/stm.ml
index a4db934b25..5edf480446 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -161,6 +161,11 @@ type step =
   | `Alias  of alias_t ]
 type visit = { step : step; next : Stateid.t }
 
+
+(* Parts of the system state that are morally part of the proof state *)
+let summary_pstate = [ Evarutil.meta_counter_summary_name;
+                       Evarutil.evar_counter_summary_name;
+                       "program-tcc-table" ]
 type state = {
   system : States.state;
   proof : Proof_global.state;
@@ -594,9 +599,12 @@ module State : sig
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
   val same_env : frozen_state -> frozen_state -> bool
+
+  type proof_part
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  val proof_part_of_frozen : frozen_state -> Proof_global.state
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
 end = struct (* {{{ *)
@@ -620,9 +628,14 @@ end = struct (* {{{ *)
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
+  type proof_part =
+    Proof_global.state * Summary.frozen_bits (* only meta counters *)
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  let proof_part_of_frozen { proof } = proof
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  let proof_part_of_frozen { proof; system } =
+    proof,
+    Summary.project_summary (States.summary_of_state system) summary_pstate
 
   let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
 
@@ -657,9 +670,16 @@ end = struct (* {{{ *)
     if VCS.get_state id <> None then () else
     try match what with
     | `Full s -> VCS.set_state id s
-    | `Proof(ontop,p) ->
-         if is_cached ontop then (
-           VCS.set_state id { (get_cached ontop) with proof = p })
+    | `Proof(ontop,(pstate,counters)) ->
+         if is_cached ontop then
+           let s = get_cached ontop in
+           let s = { s with proof = pstate } in
+           let s = { s with system =
+             States.replace_summary s.system
+               (Summary.surgery_summary
+                 (States.summary_of_state s.system)
+               counters) } in
+           VCS.set_state id s
     with VCS.Expired -> ()
 
   let exn_on id ?valid (e, info) =
@@ -1555,7 +1575,7 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+let pstate = summary_pstate
 
 let async_policy () =
   let open Flags in
-- 
cgit v1.2.3


From 550da87456ae156ced70fdb123d9f36ac7b84720 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Feb 2015 16:42:59 +0100
Subject: CoqIDE: correclty unfocus (remove all tags) when jumping out of a
 proof

---
 ide/coqOps.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8ba1c8ecd2..1800cb8fe8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -662,10 +662,14 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      buffer#remove_tag Tags.Script.read_only ~start ~stop;
+      buffer#remove_tag Tags.Script.error ~start ~stop;
+      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
-    List.iter (fun { stop } -> buffer#delete_mark stop) seg
+    List.iter (fun { stop } -> buffer#delete_mark stop) seg;
+    self#print_stack
 
   (** Wrapper around the raw undo command *)
   method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
-- 
cgit v1.2.3


From d82f2c96e73484aae7e6f9e014823065584fbc6e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 09:21:21 +0100
Subject: Moving test for bug #3681 as closed.

---
 test-suite/bugs/closed/3681.v | 20 ++++++++++++++++++++
 test-suite/bugs/opened/3681.v | 20 --------------------
 2 files changed, 20 insertions(+), 20 deletions(-)
 create mode 100644 test-suite/bugs/closed/3681.v
 delete mode 100644 test-suite/bugs/opened/3681.v

diff --git a/test-suite/bugs/closed/3681.v b/test-suite/bugs/closed/3681.v
new file mode 100644
index 0000000000..194113c6ed
--- /dev/null
+++ b/test-suite/bugs/closed/3681.v
@@ -0,0 +1,20 @@
+Module Type FOO.
+  Parameters P Q : Type -> Type.
+End FOO.
+
+Module Type BAR.
+  Declare Module Import foo : FOO.
+  Parameter f : forall A, P A -> Q A -> A.
+End BAR.
+
+Module Type BAZ.
+  Declare Module Export foo : FOO.
+  Parameter g : forall A, P A -> Q A -> A.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) : BAR.
+  Import baz.
+  Module foo <: FOO := foo.
+  Import foo.
+  Definition f : forall A, P A -> Q A -> A := g.
+End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3681.v b/test-suite/bugs/opened/3681.v
deleted file mode 100644
index 194113c6ed..0000000000
--- a/test-suite/bugs/opened/3681.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Module Type FOO.
-  Parameters P Q : Type -> Type.
-End FOO.
-
-Module Type BAR.
-  Declare Module Import foo : FOO.
-  Parameter f : forall A, P A -> Q A -> A.
-End BAR.
-
-Module Type BAZ.
-  Declare Module Export foo : FOO.
-  Parameter g : forall A, P A -> Q A -> A.
-End BAZ.
-
-Module BAR_FROM_BAZ (baz : BAZ) : BAR.
-  Import baz.
-  Module foo <: FOO := foo.
-  Import foo.
-  Definition f : forall A, P A -> Q A -> A := g.
-End BAR_FROM_BAZ.
-- 
cgit v1.2.3


From 9dacc590c604290d9556d9368c5c735321e01e90 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 09:58:46 +0100
Subject: Revert "Fixing bug #4035 (support for dependent destruction within
 ltac code)."

This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was
breaking compatibility because one could no longer use names of foralls in
the goal without introducting them. Probably not good style, but it did
break many existing developments including CompCert.

Closes #4093 but reopens #4035.
---
 test-suite/bugs/closed/4035.v |  7 -------
 theories/Program/Equality.v   | 20 ++++++++++----------
 2 files changed, 10 insertions(+), 17 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4035.v

diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
deleted file mode 100644
index 24f340bbd9..0000000000
--- a/test-suite/bugs/closed/4035.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Use of dependent destruction from ltac *)
-Require Import Program.
-Goal nat -> Type.
-  intro x.
-  lazymatch goal with
-  | [ x : nat |- _ ] => dependent destruction x
-  end.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 4b02873172..ae6fe7dd0a 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -433,40 +433,40 @@ Ltac do_depelim' rev tac H :=
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Tactic Notation "dependent" "destruction" hyp(H) := 
+Tactic Notation "dependent" "destruction" ident(H) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the elimination. *)
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
-Tactic Notation "dependent" "induction" hyp(H) :=
+Tactic Notation "dependent" "induction" ident(H) :=
   do_depind ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "using" constr(c) :=
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
   do_depind ltac:(fun hyp => induction hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) :=
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.
-- 
cgit v1.2.3


From 6fcfa31005273e3d5e0fac6fec9c0448e66a8780 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 10:04:55 +0100
Subject: Fixing complexity tests for #4076.

---
 test-suite/complexity/bug4076.v    | 2 +-
 test-suite/complexity/bug4076bis.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
index 2c87a908f4..3cf9e8b093 100644
--- a/test-suite/complexity/bug4076.v
+++ b/test-suite/complexity/bug4076.v
@@ -8,7 +8,7 @@ Unset Strict Implicit.
 Parameter f : forall P, forall (i : nat), P i -> P i.
 Parameter P : nat -> Type.
 
-Definition g (n : nat) (a0 : P n) : P n :=
+Time Definition g (n : nat) (a0 : P n) : P n :=
   let a1  := f a0 in
   let a2  := f a1 in
   let a3  := f a2 in
diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
index 9303e60a21..f3996e6ae6 100644
--- a/test-suite/complexity/bug4076bis.v
+++ b/test-suite/complexity/bug4076bis.v
@@ -8,7 +8,7 @@ Unset Strict Implicit.
 Parameter f : forall P, forall (i j : nat), P i j -> P i j.
 Parameter P : nat -> nat -> Type.
 
-Timeout 10 Definition g (n : nat) (a0 : P n n) : P n n :=
+Time Definition g (n : nat) (a0 : P n n) : P n n :=
   let a1  := f a0 in
   let a2  := f a1 in
   let a3  := f a2 in
-- 
cgit v1.2.3


From c8944dccb081c79eb47ca91c7e2cb5c50558aeaa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Feb 2015 13:13:05 +0100
Subject: Fix checker after addition of a universe context in with t := c
 constraints.

---
 checker/cic.mli         | 2 +-
 checker/declarations.ml | 2 +-
 checker/values.ml       | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/checker/cic.mli b/checker/cic.mli
index a793fefa83..90a0e9feb6 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -333,7 +333,7 @@ type ('ty,'a) functorize =
 
 type with_declaration =
   | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * constr
+  | WithDef of Id.t list * (constr * Univ.universe_context)
 
 type module_alg_expr =
   | MEident of module_path
diff --git a/checker/declarations.ml b/checker/declarations.ml
index c6709a7852..8d913475f9 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -583,7 +583,7 @@ let implem_map fs fa = function
 
 let subst_with_body sub = function
   | WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
-  | WithDef(id,c) -> WithDef(id,subst_mps sub c)
+  | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx))
 
 let rec subst_expr sub = function
   | MEident mp -> MEident (subst_mp sub mp)
diff --git a/checker/values.ml b/checker/values.ml
index 3ca44b7d0f..c986415070 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli
+MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
 
 *)
 
@@ -270,7 +270,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
 let v_with =
   Sum ("with_declaration_body",0,
        [|[|List v_id;v_mp|];
-         [|List v_id;v_constr|]|])
+         [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|])
 
 let rec v_mae =
   Sum ("module_alg_expr",0,
-- 
cgit v1.2.3


From f712a0523359d5b54b4d4160bc77271fdde094a3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 14:33:07 +0100
Subject: Mention -R option in warnings, fixing #4067 and #4068.

---
 tools/coq_makefile.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b84d15d62e..bd78fe2c54 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,8 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
   [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
-  ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value]
+  ... [-I dir] ... [-R physicalpath logicalpath]
+  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
   ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
   [-h] [--help]
 
@@ -767,10 +768,10 @@ let check_overlapping_include (_,inc_i,inc_r) =
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
+	  Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
 	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
-	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
+	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
   in aux (inc_i@inc_r)
 
 let do_makefile args =
-- 
cgit v1.2.3


From 15a3b57db10e61c9de12b5880b04b46db1494b5b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 14:31:25 +0100
Subject: Fixing printing of ordinals.

---
 lib/cString.ml     |  9 ++++++++-
 lib/pp.ml          | 11 ++++++++++-
 tactics/tactics.ml |  2 +-
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/lib/cString.ml b/lib/cString.ml
index 250b7cee2d..e9006860fd 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -135,7 +135,14 @@ let plural n s = if n<>1 then s^"s" else s
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
 
 let ordinal n =
-  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
   string_of_int n ^ s
 
 (* string parsing *)
diff --git a/lib/pp.ml b/lib/pp.ml
index cc56e5e8d7..76046a7f91 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -517,8 +517,17 @@ let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
+(** TODO: merge with CString.ordinal *)
 let pr_nth n =
-  int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th")
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
+  int n ++ str s
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 013270b0bd..ccf4795d68 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -882,7 +882,7 @@ let msg_quantified_hypothesis = function
   | NamedHyp id ->
       str "quantified hypothesis named " ++ pr_id id
   | AnonHyp n ->
-      int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+      pr_nth n ++
       str " non dependent hypothesis"
 
 let depth_of_quantified_hypothesis red h gl =
-- 
cgit v1.2.3


From b4a16a43d9f84969feb7b8b090092260cb898e23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 15:03:36 +0100
Subject: Fixing printing error in coq_makefile.

---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bd78fe2c54..84b4b5e5df 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -158,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
   |l ->
     try
       let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
-      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in
       (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
     with Not_found ->
       (
-- 
cgit v1.2.3


From 9582053a841c55010ddb2c4868f691151d4d949d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 15:32:02 +0100
Subject: Fixing bug 3099.

---
 doc/refman/Classes.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 96b486cdfa..069b991274 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -326,7 +326,8 @@ An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$}
 can be put after the name of the instance and before the colon to
 declare a parameterized instance.
 An optional \textit{priority} can be declared, 0 being the highest
-priority as for auto hints.
+priority as for auto hints. If the priority is not specified, it defaults to
+$n$, the number of binders of the instance.
 
 \begin{Variants}
 \item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
-- 
cgit v1.2.3


From 1b7d4a033af8c449877252710683f6f9494a6096 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 15:54:01 +0100
Subject: Trying to fix code locating camlp4/camlp5.

Should fix #3396 and #3964.
---
 configure.ml | 85 +++++++++++++++++++++++++++---------------------------------
 1 file changed, 38 insertions(+), 47 deletions(-)

diff --git a/configure.ml b/configure.ml
index 8667a53594..f169e71000 100644
--- a/configure.ml
+++ b/configure.ml
@@ -291,7 +291,7 @@ let args_options = Arg.align [
   "-coqdocdir", arg_string_option Prefs.coqdocdir,
     "<dir> Where to install Coqdoc style files";
   "-camldir", arg_string_option Prefs.camldir,
-    "<dir> Specifies the path to the OCaml library";
+    "<dir> Specifies the path to the OCaml binaries";
   "-lablgtkdir", arg_string_option Prefs.lablgtkdir,
     "<dir> Specifies the path to the Lablgtk library";
   "-usecamlp5", Arg.Set Prefs.usecamlp5,
@@ -359,8 +359,7 @@ type camlexec =
    mutable dep : string;
    mutable doc : string;
    mutable lex : string;
-   mutable yacc : string;
-   mutable p4 : string }
+   mutable yacc : string }
 
 (* TODO: autodetect .opt binaries ? *)
 
@@ -372,8 +371,7 @@ let camlexec =
     dep = "ocamldep";
     doc = "ocamldoc";
     lex = "ocamllex";
-    yacc = "ocamlyacc";
-    p4 = "camlp4o" }
+    yacc = "ocamlyacc" }
 
 let reset_caml_byte c o = c.byte <- o
 let reset_caml_opt c o = c.opt <- o
@@ -389,8 +387,7 @@ let rebase_camlexec dir c =
   c.dep <- Filename.concat dir c.dep;
   c.doc <- Filename.concat dir c.doc;
   c.lex <- Filename.concat dir c.lex;
-  c.yacc <- Filename.concat dir c.yacc;
-  c.p4 <- Filename.concat dir c.p4
+  c.yacc <- Filename.concat dir c.yacc
 
 let coq_debug_flag = if !Prefs.debug then "-g" else ""
 let coq_profile_flag = if !Prefs.profile then "-p" else ""
@@ -537,11 +534,6 @@ let camltag = match caml_version_list with
 
 (** * CamlpX configuration *)
 
-(** We assume that camlp(4|5) binaries are at the same place as ocaml ones
-    (this should become configurable some day). *)
-
-let camlp4bin = camlbin
-
 (* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
 (* TODO: remove the late attempts at finding gramlib.cma *)
 
@@ -564,7 +556,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
         camllib/"site-lib"/"camlp5"
       else ""
     in
-    (* if the two values are different than camlp5 has been relocated
+    (* if the two values are different then camlp5 has been relocated
      * and will not be able to find its own files, so we prefer the
      * path where the files actually do exist *)
     if dir2 = "" then
@@ -576,39 +568,39 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
     else dir2
 
 let check_camlp5_version () =
-  let s = camlexec.p4 in
-  (* translate 4 into 5 in the binary name *)
-  for i = 0 to String.length s - 1 do
-    if s.[i] = '4' then s.[i] <- '5'
-  done;
   try
-    let version_line, _ = run ~err:StdOut camlexec.p4 ["-v"] in
+    let camlp5o = which "camlp5o" in
+    let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
     let version = List.nth (string_split ' ' version_line) 2 in
     match string_split '.' version with
     | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
-      printf "You have Camlp5 %s. Good!\n" version
+      printf "You have Camlp5 %s. Good!\n" version; camlp5o
     | _ -> failwith "bad version"
-  with _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
+  with
+  | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
+  | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
 
 let config_camlpX () =
   try
     if not !Prefs.usecamlp5 then raise NoCamlp5;
-    let lib = "gramlib" in
-    let dir = check_camlp5 (lib^".cma") in
-    let () = check_camlp5_version () in
-    "camlp5", dir, lib
+    let camlp5mod = "gramlib" in
+    let camlp5libdir = check_camlp5 (camlp5mod^".cma") in
+    let camlp5o = check_camlp5_version () in
+    "camlp5", camlp5o, Filename.basename camlp5o, camlp5libdir, camlp5mod
   with NoCamlp5 ->
     (* We now try to use Camlp4, either by explicit choice or
        by lack of proper Camlp5 installation *)
-    let lib = "camlp4lib" in
-    let dir = camllib/"camlp4" in
-    if not (Sys.file_exists (dir/lib^".cma")) then
+    let camlp4mod = "camlp4lib" in
+    let camlp4libdir = camllib/"camlp4" in
+    if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then
       die "No Camlp4 installation found.\n";
-    let () = camlexec.p4 <- camlexec.p4 ^ "rf" in
-    ignore (run camlexec.p4 []);
-    "camlp4", dir, lib
+    try
+      let camlp4orf = which "camlp4orf" in
+      ignore (run camlp4orf []);
+      "camlp4", camlp4orf, Filename.basename camlp4orf, camlp4libdir, camlp4mod
+    with _ -> die "No Camlp4 installation found.\n"
 
-let camlp4, fullcamlp4lib, camlp4mod = config_camlpX ()
+let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod = config_camlpX ()
 
 let shorten_camllib s =
   if starts_with s (camllib^"/") then
@@ -616,8 +608,7 @@ let shorten_camllib s =
     "+" ^ String.sub s l (String.length s - l)
   else s
 
-let camlp4lib = shorten_camllib fullcamlp4lib
-
+let camlpXlibdir = shorten_camllib fullcamlpXlibdir
 
 (** * Native compiler *)
 
@@ -627,8 +618,8 @@ let msg_byteonly () =
 let msg_no_ocamlopt () =
   printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly ()
 
-let msg_no_camlp4_cmxa () =
-  printf "Cannot find the native-code library of %s.\n" camlp4; msg_byteonly ()
+let msg_no_camlpX_cmxa () =
+  printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly ()
 
 let msg_no_dynlink_cmxa () =
   printf "Cannot find native-code dynlink library.\n"; msg_byteonly ();
@@ -643,8 +634,8 @@ let check_native () =
     reset_caml_opt camlexec camloptopt
   else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then
     (msg_no_ocamlopt (); raise Not_found);
-  if not (Sys.file_exists (fullcamlp4lib/camlp4mod^".cmxa")) then
-    (msg_no_camlp4_cmxa (); raise Not_found);
+  if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) then
+    (msg_no_camlpX_cmxa (); raise Not_found);
   if not (Sys.file_exists (camllib/"dynlink.cmxa")) then
     (msg_no_dynlink_cmxa (); raise Not_found);
   let version, _ = run camlexec.opt ["-version"] in
@@ -969,7 +960,7 @@ let print_summary () =
   pr "  OCaml/Camlp4 version        : %s\n" caml_version;
   pr "  OCaml/Camlp4 binaries in    : %s\n" camlbin;
   pr "  OCaml library in            : %s\n" camllib;
-  pr "  Camlp4 library in           : %s\n" camlp4lib;
+  pr "  %s library in           : %s\n"     (String.capitalize camlpX) camlpXlibdir;
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
@@ -1009,7 +1000,7 @@ let write_dbg_wrapper f =
   pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n";
   pr "export COQTOP=%S\n" coqtop;
   pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug");
-  pr "CAMLP4LIB=%S\n\n" camlp4lib;
+  pr "CAMLP4LIB=%S\n\n" camlpXlibdir;
   pr ". $COQTOP/dev/ocamldebug-coq.run\n";
   close_out o;
   Unix.chmod f 0o555
@@ -1048,10 +1039,10 @@ let write_configml f =
   pr_s "ocamllex" camlexec.lex;
   pr_s "camlbin" camlbin;
   pr_s "camllib" camllib;
-  pr_s "camlp4" camlp4;
-  pr_s "camlp4o" camlexec.p4;
-  pr_s "camlp4bin" camlp4bin;
-  pr_s "camlp4lib" camlp4lib;
+  pr_s "camlp4" camlpX;
+  pr_s "camlp4o" camlpXo;
+  pr_s "camlp4bin" camlpXbindir;
+  pr_s "camlp4lib" camlpXlibdir;
   pr_s "camlp4compat" camlp4compat;
   pr_s "cflags" cflags;
   pr_s "best" best_compiler;
@@ -1159,10 +1150,10 @@ let write_makefile f =
   pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag;
   pr "# Camlp4 : flavor, binaries, libraries ...\n";
   pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
-  pr "CAMLP4=%s\n" camlp4;
-  pr "CAMLP4O=%S\n" camlexec.p4;
+  pr "CAMLP4=%s\n" camlpX;
+  pr "CAMLP4O=%S\n" camlpXo;
   pr "CAMLP4COMPAT=%s\n" camlp4compat;
-  pr "MYCAMLP4LIB=%S\n\n" camlp4lib;
+  pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir;
   pr "# Your architecture\n";
   pr "# Can be obtain by UNIX command arch\n";
   pr "ARCH=%s\n" arch;
-- 
cgit v1.2.3


From 31846ce3bb4053a4fd121afd6aa8260b0c5dff18 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 17:08:43 +0100
Subject: Fixing bug #3298.

---
 tactics/eauto.ml4 | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 30c5e686a9..3d98bc6e19 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -125,6 +125,14 @@ let unify_e_resolve poly flags (c,clenv) gls =
     tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
       (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
 
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none db
+  | Some hdc ->
+    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
+    else (fun db -> Hint_db.map_auto hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
 let e_exact poly flags (c,clenv) =
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
@@ -145,16 +153,11 @@ let rec e_trivial_fail_db db_list local_db goal =
     tclFIRST (List.map tclCOMPLETE tacl) goal
 
 and e_my_find_search db_list local_db hdc concl =
+  let hint_of_db = hintmap_of hdc concl in
   let hintl =
-    if occur_existential concl then
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
-   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
-    else
-      List.map_append (fun db ->
-	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -175,17 +178,14 @@ and e_my_find_search db_list local_db hdc concl =
   List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
-  try
-    priority
-      (e_my_find_search db_list local_db
-	 (decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try priority (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd
-    (e_my_find_search db_list local_db
-	(decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try List.map snd (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let find_first_goal gls =
   try first_goal gls with UserError _ -> assert false
-- 
cgit v1.2.3


From bc7d29e4c0f53d5c8e654157c4137c7e82910a7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 17:22:41 +0100
Subject: Test for bug #3298.

---
 test-suite/bugs/closed/3298.v | 21 +++++++++++++++++++++
 test-suite/bugs/opened/3298.v | 23 -----------------------
 2 files changed, 21 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/3298.v
 delete mode 100644 test-suite/bugs/opened/3298.v

diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v
new file mode 100644
index 0000000000..3a7de45670
--- /dev/null
+++ b/test-suite/bugs/closed/3298.v
@@ -0,0 +1,21 @@
+Module JGross.
+  Hint Extern 1 => match goal with |- match ?E with end => case E end.
+
+  Goal forall H : False, match H return Set with end.
+  Proof.
+    intros.
+    solve [ eauto ].
+  Qed.
+End JGross.
+
+Section BenDelaware.
+  Hint Extern 0 => admit.
+  Goal forall (H : False), id (match H return Set with end).
+  Proof.
+    eauto.
+  Qed.
+  Goal forall (H : False), match H return Set with end.
+  Proof.
+    solve [ eauto ] .
+  Qed.
+End BenDelaware.
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
deleted file mode 100644
index bce7c3f23b..0000000000
--- a/test-suite/bugs/opened/3298.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Module JGross.
-  Hint Extern 1 => match goal with |- match ?E with end => case E end.
-
-  Goal forall H : False, match H return Set with end.
-  Proof.
-    intros.
-    Fail solve [ eauto ]. (* No applicable tactic *)
-    admit.
-  Qed.
-End JGross.
-
-Section BenDelaware.
-  Hint Extern 0 => admit.
-  Goal forall (H : False), id (match H return Set with end).
-  Proof.
-    eauto.
-  Qed.
-  Goal forall (H : False), match H return Set with end.
-  Proof.
-    Fail solve [ eauto ] .
-    admit.
-  Qed.
-End BenDelaware.
-- 
cgit v1.2.3