aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Cases.v7
-rw-r--r--test-suite/success/Check.v2
-rw-r--r--test-suite/success/Compat84.v19
-rw-r--r--test-suite/success/Field.v2
-rw-r--r--test-suite/success/Tauto.v2
-rw-r--r--test-suite/success/TestRefine.v2
-rw-r--r--test-suite/success/apply.v2
-rw-r--r--test-suite/success/auto.v89
-rw-r--r--test-suite/success/destruct.v8
-rw-r--r--test-suite/success/eauto.v2
-rw-r--r--test-suite/success/eqdecide.v2
-rw-r--r--test-suite/success/extraction.v2
-rw-r--r--test-suite/success/inds_type_sec.v2
-rw-r--r--test-suite/success/induct.v2
-rw-r--r--test-suite/success/keyedrewrite.v38
-rw-r--r--test-suite/success/mutual_ind.v2
-rw-r--r--test-suite/success/primitiveproj.v16
-rw-r--r--test-suite/success/remember.v13
-rw-r--r--test-suite/success/unfold.v2
-rw-r--r--test-suite/success/univers.v17
20 files changed, 200 insertions, 31 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e42663505d..49c465b6c6 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1861,3 +1861,10 @@ Type (fun n => match n with
Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
match p with eq_refl => u end.
+
+(* Check in-pattern clauses with constant constructors, which were
+ previously interpreted as variables (before 8.5) *)
+
+Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
+
+Check match niln in listn O return O=O with niln => eq_refl end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 87c38cfa06..e4ee351c3a 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 0000000000..db6348fa17
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Goal True.
+ solve [ constructor 1 ]. Undo.
+ solve [ econstructor 1 ]. Undo.
+ solve [ constructor ]. Undo.
+ solve [ econstructor ]. Undo.
+ solve [ constructor (fail) ]. Undo.
+ solve [ econstructor (fail) ]. Undo.
+ split.
+Qed.
+
+Goal False \/ True.
+ solve [ constructor (constructor) ]. Undo.
+ solve [ econstructor (econstructor) ]. Undo.
+ solve [ constructor 2; constructor ]. Undo.
+ solve [ econstructor 2; econstructor ]. Undo.
+ right; esplit.
+Qed.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 8db08b6d78..438e461357 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 01d9afb426..767f15be72 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 3090f40cde..c8a8b862fa 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b723..02e043bc36 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
exists x, exists y, X x y.
Proof.
-intros; eexists; eexists; case H.
+intros; eexists; eexists ?[y]; case H.
apply (foo ?y).
Grab Existential Variables.
exact 0.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index aaa7b3a514..5477c83316 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -45,3 +45,92 @@ Proof.
eexists. Fail progress debug eauto with test2.
progress eauto with test.
Qed.
+
+(** Patterns of Extern have a "matching" semantics.
+ It is not so for apply/exact hints *)
+
+Class B (A : Type).
+Class I.
+Instance i : I.
+
+Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
+Class D (f : nat -> nat -> nat).
+Definition ftest (x y : nat) := x + y.
+Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
+ Admitted.
+Module Instnopat.
+ Local Instance: B nat.
+ (* pattern_of_constr -> B nat *)
+ (* exact hint *)
+ Check (_ : B nat).
+ (* map_eauto -> B_instance0 *)
+ (* NO Constr_matching.matches !!! *)
+ Check (_ : B _).
+
+ Goal exists T, B T.
+ eexists.
+ eauto with typeclass_instances.
+ Qed.
+
+ Local Instance: D ftest.
+ Local Hint Resolve flipD | 0 : typeclass_instances.
+ (* pattern: D (flip _) *)
+ Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)
+
+End Instnopat.
+
+Module InstnopatApply.
+ Local Instance: I -> B nat.
+ (* pattern_of_constr -> B nat *)
+ (* apply hint *)
+ Check (_ : B nat).
+ (* map_eauto -> B_instance0 *)
+ (* NO Constr_matching.matches !!! *)
+ Check (_ : B _).
+
+ Goal exists T, B T.
+ eexists.
+ eauto with typeclass_instances.
+ Qed.
+End InstnopatApply.
+
+Module InstPat.
+ Hint Extern 3 (B nat) => split : typeclass_instances.
+ (* map_eauto -> Extern hint *)
+ (* Constr_matching.matches -> true *)
+ Check (_ : B nat).
+ (* map_eauto -> Extern hint *)
+ (* Constr_matching.matches -> false:
+ Because an inductive in the pattern does not match an evar in the goal *)
+ Check (_ : B _).
+
+ Goal exists T, B T.
+ eexists.
+ (* map_existential -> Extern hint *)
+ (* Constr_matching.matches -> false *)
+ Fail progress eauto with typeclass_instances.
+ (* map_eauto -> Extern hint *)
+ (* Constr_matching.matches -> false *)
+ Fail typeclasses eauto.
+ Abort.
+
+ Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
+ Module withftest.
+ Local Instance: D ftest.
+
+ Check (_ : D _).
+ (* D_instance_0 : D ftest *)
+ Check (_ : D (flip _)).
+ (* ... : D (flip ftest) *)
+ End withftest.
+ Module withoutftest.
+ Hint Extern 0 (D ftest) => split : typeclass_instances.
+ Check (_ : D _).
+ (* ? : D ?, _not_ looping *)
+ Check (_ : D (flip _)).
+ (* ? : D (flip ?), _not_ looping *)
+
+ Check (_ : D (flip ftest)).
+ (* flipD ftest {| |} : D (flip ftest) *)
+ End withoutftest.
+End InstPat.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f091e3996..90a60daa66 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,21 +96,21 @@ Abort.
(* Check that subterm selection does not solve existing evars *)
Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
Show x. (* Incidentally test Show on a named goal *)
destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
change (0 = S 0).
Abort.
Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
change (0 = S ?x).
[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
Abort.
Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
Abort.
@@ -426,7 +426,7 @@ destruct b eqn:H.
(* Check natural instantiation behavior when the goal has already an evar *)
Goal exists x, S x = x.
-eexists.
+eexists ?[x].
destruct (S _).
change (0 = ?x).
Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 9e57801e06..773dd321eb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1b5c7f183e..1f6af0dc44 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 57f3775d7e..0086e090bd 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index b733aef6db..c729b23ce7 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 7ae60d9892..b8c6bf3ff7 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index bbe9d4bfff..b88c142be1 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -22,3 +22,41 @@ Qed.
Print Equivalent Keys.
End foo.
+
+Require Import Arith List Omega.
+
+Definition G {A} (f : A -> A -> A) (x : A) := f x x.
+
+Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l.
+Proof. unfold G; rewrite app_nil_r; reflexivity. Qed.
+
+(* Bundled version of a magma *)
+Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }.
+Arguments op {_} _ _.
+
+(* Instance for lists *)
+Canonical Structure list_magma A := Magma (list A) (@app A).
+
+(* Basically like list_foo, but now uses the op projection instead of app for
+the argument of G *)
+Lemma test1 A (l : list A) : G op (l ++ nil) = G op l.
+
+(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *)
+rewrite -> list_foo.
+reflexivity.
+Qed.
+
+(* Basically like list_foo, but now uses the op projection for everything *)
+Lemma test2 A (l : list A) : G op (op l nil) = G op l.
+Proof.
+rewrite ->list_foo.
+reflexivity.
+Qed.
+
+ Require Import Bool.
+ Set Keyed Unification.
+
+ Lemma test b : b && true = b.
+ Fail rewrite andb_true_l.
+ Admitted.
+ \ No newline at end of file
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 54cfa658c8..45c1a5e584 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb3..b5e6ccd618 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
Check nat.
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
Check _.(next) : option Y.
Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y :=
- match n with
- | 0 => t
- | S n => {| next := Some (yn n y) |}
- end.
+Proof. Fail reflexivity. Abort.
-Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
(*
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a3..b26a9ff1eb 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
remember (1 + 2) as x eqn:name.
rewrite fresh.
Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.
+
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 2954e25562..d595cbc2b8 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb68..269359ae62 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
(* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+ myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+ BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec. \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:27:36 +0000