Merge branch 'v8.6'

13 files changed, 121 insertions, 49 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index b32071e802..c10cd4ed44 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
+PREREQUISITELOG = prerequisite/admit.v.log			\
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
 #######################################################################
 # Phony targets
 #######################################################################
@@ -102,7 +105,7 @@ run: $(SUBSYSTEMS)
 bugs: $(BUGS)
 
 clean:
-	rm -f trace lia.cache
+	rm -f trace .lia.cache
 	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
 	$(HIDE)find . \( \
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
@@ -226,7 +229,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 $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -257,7 +260,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 $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -271,7 +274,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 $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	  rm $$tmpexpected; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -348,7 +351,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 $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -379,7 +382,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 $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v
new file mode 100644
index 0000000000..102a2aba0d
--- /dev/null
+++ b/test-suite/bugs/closed/3495.v
@@ -0,0 +1,18 @@
+Require Import RelationClasses.
+
+Axiom R : Prop -> Prop -> Prop.
+Declare Instance : Reflexive R.
+
+Class bar := { x : False }.
+Record foo := { a : Prop ; b : bar }.
+
+Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
+
+Goal exists k, R k True.
+Proof.
+eexists.
+evar (b : bar).
+let e := match goal with |- R ?e _ => constr:(e) end in
+unify e (a (default_foo True)).
+subst b.
+reflexivity.
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 4ca6fe78cd..08628377f0 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -249,10 +249,10 @@ Section Reflective_Subuniverse.
  exact H.
     Defined.
 
-    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
+    Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
 S)    : In@{Ou Oa i} O (x=y).
     Proof.
-      simple refine (inO_to_O_retract@{i j} _ _ _); intro u.
+      simple refine (inO_to_O_retract@{i} _ _ _); intro u.
       -
  assert (p : (fun _ : O (x=y) => x) == (fun _=> y)).
         {
@@ -264,4 +264,4 @@ S)    : In@{Ou Oa i} O (x=y).
  hnf.
         rewrite O_indpaths_beta; reflexivity.
     Qed.
-    Check inO_paths@{Type Type}.
+    Check inO_paths@{Type}.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 048f31ce3d..da140c9318 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -652,7 +652,7 @@ Defined.
 
   Definition ReflectiveSubuniverse := Modality.
 
-  Definition O_reflector := O_reflector.
+  Definition O_reflector@{u a i} := O_reflector@{u a i}.
 
   Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
                    Type2le@{i a} -> Type2le@{i a}
@@ -660,7 +660,7 @@ Defined.
   Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
                                In@{u a i} O (O_reflector@{u a i} O T)
     := O_inO@{u a i}.
-  Definition to := to.
+  Definition to@{u a i} := to@{u a i}.
   Definition inO_equiv_inO@{u a i j k} :
       forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
              (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
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
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.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 2b828d382a..8ce6f9795c 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,19 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern 
+gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 3c2eaf42c9..4074896420 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -77,3 +77,32 @@ destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+   general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+  match x with
+  | gadtNat n => gadtNat n
+  end.
+
+(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *)
+
+Inductive type:Set:=Nat.
+Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat.
+Inductive texp:type->Set:=
+ |TNConst:nat->texp Nat
+ |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t.
+Definition typeDenote(t:type):Set:= match t with Nat => nat end.
+
+(* We expect a failure on TBinop *)
+Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
+  match e with
+  | TNConst n => n
+  | TBinop t1 t2 _ b e1 e2 => O
+  end.
+
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1eb7eca8f1..f3c12effca 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
 Nat.ldiff: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-
 S: nat -> nat
 Nat.succ: nat -> nat
 Nat.pred: nat -> nat
@@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-
 h: n <> newdef n
 h: n <> newdef n
 h: P n
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index f4254e4e2f..a7bde5ea3f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -26,3 +26,8 @@ The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
 Error: No primitive equality found.
+Hx
+nat
+nat
+0
+0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index dfa60eeda0..76c37625aa 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -43,3 +43,17 @@ Goal True -> False.
 Fail h I.
 intro H.
 Fail h H.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+
+(* Check consistency of interpretation scopes (#4398) *)
+
+Goal nat*(0*0=0) -> nat*(0*0=0). intro.
+match goal with H: ?x*?y |- _ => idtac x end.
+match goal with |- ?x*?y => idtac x end.
+match goal with H: context [?x*?y] |- _ => idtac x end.
+match goal with |- context [?x*?y] => idtac x end.
+Abort.
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
index d152052ba3..ae84603622 100644
--- a/test-suite/output/unifconstraints.out
+++ b/test-suite/output/unifconstraints.out
@@ -8,11 +8,7 @@ subgoal 2 is:
  forall n : nat, ?Goal n -> ?Goal (S n)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal ?Goal2 <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal ?Goal2 <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -28,11 +24,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -48,12 +40,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
    True /\ True /\ True \/
@@ -70,12 +57,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
    True /\ True /\ True \/
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 30abd961b1..07bbb60c40 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -115,3 +115,16 @@ Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
 Require Import Coq.Vectors.VectorDef.
 Import VectorNotations.
 Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
+Check |- {{ 0 }} 0.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.