Merge commit 'e6edb33' into v8.6

Was PR#331: Solve_constraints and Set Use Unification Heuristics

6 files changed, 88 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859edd..7fae32871 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. refine (Cons (cast H _ y)).
\ No newline at end of file
+  intros. Fail refine (Cons (cast H _ y)).
+  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
+  refine (Cons (cast H _ y)).
+  intros.
+  refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index 495e67e09..f5a22bd50 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -650,4 +650,5 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
 
   Grab Existential Variables.
   subst_body; simpl.
-  refine (all_behead (projT2 _)).
+  Fail refine (all_behead (projT2 _)).
+  Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce64..3189685ec 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 000000000..ae8ed0e6e
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+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
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 000000000..684dba196
--- /dev/null
+++ b/test-suite/bugs/closed/5149.v
@@ -0,0 +1,47 @@
+Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
+intros.
+eexists.
+rewrite <- H.
+eassumption.
+Qed.
+
+Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) 
+            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : 
+flat_type -> Type)
+            (v v' : interp_flat_type1 t'),
+    v = v' ->
+    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
+           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> 
+interp_flat_type0 t0)
+           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
+           (x' : interp_flat_type1 (Tbase t)) (T : Type)
+           (flatten_binding_list : forall t0 : flat_type,
+               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
+           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
+           (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) 
+(interp_flat_type1 (Tbase x0)) -> T)
+           (pair : forall A B : Type, A -> B -> prod A B),
+      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
+        (flatten_binding_list t' (SmartVarVar t' v') v) ->
+      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 
+t'0)
+              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
+          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 
+x'0))
+            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf 
+(Tbase t0) x0 = x'0) ->
+      interpf (Tbase t) x = x'.
+Proof.
+  intros ?????????????????????? interpf_SmartVarVar.
+  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail 
+"too early".
+  Undo.
+  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
+  solve [eapply interpf_SmartVarVar; subst; eassumption].
+  Undo.
+  Unset Solve Unification Constraints.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
index 5fbcfef4e..de60fd0ae 100644
--- a/test-suite/bugs/closed/HoTT_coq_117.v
+++ b/test-suite/bugs/closed/HoTT_coq_117.v
@@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A,
 Admitted.
 
 Inductive Empty : Set := .
-Instance contr_from_Empty {_ : Funext} (A : Type) :
+Fail Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+Fail Instance contr_from_Empty {F : Funext} (A : Type) :
   Contr_internal (Empty -> A) :=
   BuildContr _
              (Empty_rect (fun _ => A))
              (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+(** This could be disallowed, this uses the Funext argument *)
+Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
+
+Instance contr_from_Empty' {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
 (* Toplevel input, characters 15-220:
 Anomaly: unknown meta ?190. Please report. *)