From e6f6cff7b88a70fe694507efe12885a776ab6730 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 12:07:38 +0200
Subject: Change the order of arguments of fig2dev.

For some reason, with my version of transfig (which seems to be the latest),
the order of arguments of the fig2dev command matters: -L png must come
before -m 2. I suppose that this fix shouldn't break things for others.
---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.doc b/Makefile.doc
index b7251ce579..cea6f9b1a5 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -61,7 +61,7 @@ endif
 	(cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`)
 
 %.png: %.fig
-	$(FIG2DEV) -m 2 -L png $< $@
+	$(FIG2DEV) -L png -m 2 $< $@
 
 %.pdf: %.fig
 	$(FIG2DEV) -L pdftex $< $@
-- 
cgit v1.2.3


From a07f67f6f1deba8b14672c618c003ec345d7970a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Sep 2016 16:37:04 +0200
Subject: A fix for #5097 (status of evars refined by "clear" in ltac: closed
 wrt evars).

If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.

If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
---
 pretyping/evarutil.ml         | 22 ++++++++++++++++++++++
 pretyping/evarutil.mli        |  6 ++++++
 pretyping/pretyping.ml        | 31 ++++++++++++++++++-------------
 proofs/proofview.ml           | 36 ++++++------------------------------
 test-suite/bugs/closed/5097.v |  7 +++++++
 5 files changed, 59 insertions(+), 43 deletions(-)
 create mode 100644 test-suite/bugs/closed/5097.v

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 759e0e4d6d..9a9c946aeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -600,6 +600,28 @@ let gather_dependent_evars evm l =
 
 (* /spiwack *)
 
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+    the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially)
+    solved. *)
+(* spiwack: [advance] is probably performance critical, and the good
+   behaviour of its definition may depend sensitively to the actual
+   definition of [Evd.find]. Currently, [Evd.find] starts looking for
+   a value in the heap of undefined variable, which is small. Hence in
+   the most common case, where [advance] is applied to an unsolved
+   goal ([advance] is used to figure if a side effect has modified the
+   goal) it terminates quickly. *)
+let rec advance sigma evk =
+  let evi = Evd.find sigma evk in
+  match evi.evar_body with
+  | Evar_empty -> Some evk
+  | Evar_defined v ->
+      if Option.default false (Store.get evi.evar_extra cleared) then
+        let (evk,_) = Term.destEvar v in
+        advance sigma evk
+      else
+        None
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f68651a74e..b60daae6d0 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -123,6 +123,12 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
     its (partial) definition. *)
 val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
 
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+    the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially)
+    solved. *)
+val advance : evar_map -> evar -> evar option
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2e164e540a..c4ea79f954 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,17 +183,24 @@ type inference_flags = {
   expand_evars : bool
 }
 
-let frozen_holes (sigma, sigma') =
-  (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
-
-let pending_holes (sigma, sigma') =
-  let fold evk _ accu =
-    if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
-  in
-  Evd.fold_undefined fold sigma' Evar.Set.empty
+(* Compute the set of still-undefined initial evars up to restriction
+   (e.g. clearing) and the set of yet-unsolved evars freshly created
+   in the extension [sigma'] of [sigma] (excluding the restrictions of
+   the undefined evars of [sigma] to be freshly created evars of
+   [sigma']). Otherwise said, we partition the undefined evars of
+   [sigma'] into those already in [sigma] or deriving from an evar in
+   [sigma] by restriction, and the evars properly created in [sigma'] *)
+
+let frozen_and_pending_holes (sigma, sigma') =
+  let add_derivative_of evk evi acc =
+    match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+  let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
+  let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+  let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+  (frozen,pending)
 
 let apply_typeclasses env evdref frozen fail_evar =
-  let filter_frozen = frozen in
+  let filter_frozen evk = Evar.Set.mem evk frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -244,8 +251,7 @@ let check_evars_are_solved env current_sigma frozen pending =
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma pending =
-  let frozen = frozen_holes pending in
-  let pending = pending_holes pending in
+  let frozen,pending = frozen_and_pending_holes pending in
   let evdref = ref current_sigma in
   if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
@@ -255,8 +261,7 @@ let solve_remaining_evars flags env current_sigma pending =
   !evdref
 
 let check_evars_are_solved env current_sigma pending =
-  let frozen = frozen_holes pending in
-  let pending = pending_holes pending in
+  let frozen,pending = frozen_and_pending_holes pending in
   check_evars_are_solved env current_sigma frozen pending
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 2fc4042354..46a370d530 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -146,33 +146,9 @@ let focus i j sp =
   let (new_comb, context) = focus_sublist i j sp.comb in
   ( { sp with comb = new_comb } , context )
 
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-    the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially)
-    solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let open Evd in
-  let evi = Evd.find sigma g in
-  match evi.evar_body with
-  | Evar_empty -> Some g
-  | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
 (** [undefined defs l] is the list of goals in [l] which are still
     unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (advance defs) l
+let undefined defs l = CList.map_filter (Evarutil.advance defs) l
 
 (** Unfocuses a proofview with respect to a context. *)
 let unfocus c sp =
@@ -429,7 +405,7 @@ let iter_goal i =
   Comb.get >>= fun initial ->
   Proof.List.fold_left begin fun (subgoals as cur) goal ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -453,7 +429,7 @@ let fold_left2_goal i s l =
   in 
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -497,7 +473,7 @@ let tclDISPATCHGEN0 join tacs =
         let open Proof in
         Pv.get >>= function
         | { comb=[goal] ; solution } ->
-            begin match advance solution goal with
+            begin match Evarutil.advance solution goal with
             | None -> tclUNIT (join [])
             | Some _ -> Proof.map (fun res -> join [res]) tac
             end
@@ -1012,7 +988,7 @@ module Goal = struct
     Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
-      match advance sigma goal with
+      match Evarutil.advance sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
@@ -1026,7 +1002,7 @@ module Goal = struct
 
   let unsolved { self=self } =
     tclEVARMAP >>= fun sigma ->
-    tclUNIT (not (Option.is_empty (advance sigma self)))
+    tclUNIT (not (Option.is_empty (Evarutil.advance sigma self)))
 
   (* compatibility *)
   let goal { self=self } = self
diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v
new file mode 100644
index 0000000000..37b239cf61
--- /dev/null
+++ b/test-suite/bugs/closed/5097.v
@@ -0,0 +1,7 @@
+(* Tracing existing evars along the weakening rule ("clear") *)
+Goal forall y, exists x, x=0->x=y.
+intros.
+eexists ?[x].
+intros.
+let x:=constr:(ltac:(clear y; exact 0)) in idtac x.
+Abort.
-- 
cgit v1.2.3


From 6d5fe92efbe3f6269666644a0f2e8e9aab8ab307 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Oct 2016 10:08:49 +0200
Subject: Adding dependency of the test-suite subsystems in prerequisite
 (fixing #5150).

---
 test-suite/Makefile | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f1cb21ecd5..8500ef1b3d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -221,7 +221,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -253,7 +253,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -267,7 +267,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -289,7 +289,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	  rm $$tmpoutput; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -307,7 +307,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -338,7 +338,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-- 
cgit v1.2.3


From 5609da1e08f950fab85b87b257ed343b491f1ef5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Oct 2016 17:57:18 +0200
Subject: Revert "unification.ml: fix for bug #4763, unif regression"

This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.

A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
---
 pretyping/evarsolve.ml        |  2 --
 pretyping/unification.ml      |  3 ++-
 test-suite/bugs/closed/4763.v | 13 -------------
 3 files changed, 2 insertions(+), 16 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4763.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4a99246bba..d639208fb4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1588,8 +1588,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
  * ass.
  *)
 
-(* This criterion relies on the fact that we postpone only problems of the form:
-?x [?x1 ... ?xn] = t or the symmetric case. *)
 let status_changed lev (pbty,_,t1,t2) =
   (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
   (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b7edd6fcd6..9f8238513e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1244,7 +1244,8 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
-  | Success evd -> evd
+  | Success evd ->
+      Evarconv.consider_remaining_unif_problems env evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
deleted file mode 100644
index ae8ed0e6e8..0000000000
--- a/test-suite/bugs/closed/4763.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
-Coercion is_true : bool >-> Sortclass.
-Global Instance: Transitive leb.
-Admitted.
-
-Goal forall x y z, leb x y -> leb y z -> True.
-  intros ??? H H'.
-  lazymatch goal with
-  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
-    => pose proof (transitivity H H' : is_true (R x z))
-  end.
-  exact I.
-Qed.
\ No newline at end of file
-- 
cgit v1.2.3