Update test-suite files after last commit. Add a file for rewrite_strat

examples.

5 files changed, 161 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3309.v b/test-suite/bugs/closed/3309.v
index fcebdec728..fcebdec728 100644
--- a/test-suite/bugs/opened/3309.v
+++ b/test-suite/bugs/closed/3309.v
diff --git a/test-suite/bugs/closed/3567.v b/test-suite/bugs/closed/3567.v
new file mode 100644
index 0000000000..cb16b3ae4a
--- /dev/null
+++ b/test-suite/bugs/closed/3567.v
@@ -0,0 +1,68 @@
+
+(* File reduced by coq-bug-finder from original input, then from 2901 lines to 69 lines, then from 80 lines to 63 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 2 2014 2:7:1 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (3c5daf4e23ee20f0788c0deab688af452e83ccf0) *)
+
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments fst {A B} _ / .
+Arguments snd {A B} _ / .
+Add Printing Let prod.
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Unset Implicit Arguments.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+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 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) :=
+  { 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) }.
+Definition path_prod_uncurried {A B : Type} (z z' : A * B) (pq : (fst z = fst z') * (snd z = snd z'))
+: (z = z')
+  := match fst pq in (_ = z'1), snd pq in (_ = z'2) return z = (z'1, z'2) with
+       | idpath, idpath => idpath
+     end.
+Definition path_prod {A B : Type} (z z' : A * B) :
+  (fst z = fst z') -> (snd z = snd z') -> (z = z')
+  := fun p q => path_prod_uncurried z z' (p,q).
+Definition path_prod' {A B : Type} {x x' : A} {y y' : B}
+: (x = x') -> (y = y') -> ((x,y) = (x',y'))
+  := fun p q => path_prod (x,y) (x',y') p q.
+Axiom ap_fst_path_prod : forall {A B : Type} {z z' : A * B}
+                                (p : fst z = fst z') (q : snd z = snd z'),
+                           ap fst (path_prod _ _ p q) = p.
+Axiom ap_snd_path_prod : forall {A B : Type} {z z' : A * B}
+                                (p : fst z = fst z') (q : snd z = snd z'),
+                           ap snd (path_prod _ _ p q) = q.
+Axiom eta_path_prod : forall {A B : Type} {z z' : A * B} (p : z = z'),
+                        path_prod _ _(ap fst p) (ap snd p) = p.
+Definition isequiv_path_prod {A B : Type} {z z' : A * B} : IsEquiv (path_prod_uncurried z z').
+Proof.
+  refine (Build_IsEquiv
+            _ _ _
+            (fun r => (ap fst r, ap snd r))
+            eta_path_prod
+            (fun pq => match pq with
+                         | (p,q) => path_prod'
+                                      (ap_fst_path_prod p q) (ap_snd_path_prod p q)
+                       end) _).
+  destruct z as [x y], z' as [x' y']. simpl.
+(* Toplevel input, characters 15-50:
+Error: Abstracting over the term "z" leads to a term
+fun z0 : A * B =>
+forall x : (fst z0 = fst z') * (snd z0 = snd z'),
+eta_path_prod (path_prod_uncurried z0 z' x) =
+ap (path_prod_uncurried z0 z')
+  (let (p, q) as pq
+       return
+         ((ap (fst) (path_prod_uncurried z0 z' pq),
+          ap (snd) (path_prod_uncurried z0 z' pq)) = pq) := x in
+   path_prod' (ap_fst_path_prod p q) (ap_snd_path_prod p q))
+which is ill-typed.
+Reason is: Pattern-matching expression on an object of inductive type prod
+has invalid information.
+ *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3624.v b/test-suite/bugs/closed/3624.v
new file mode 100644
index 0000000000..a05d5eb215
--- /dev/null
+++ b/test-suite/bugs/closed/3624.v
@@ -0,0 +1,11 @@
+Set Implicit Arguments.
+Module NonPrim.
+  Class foo (m : Set) := { pf : m = m }.
+  Notation pf' m := (pf (m := m)).
+End NonPrim.
+
+Module Prim.
+  Set Primitive Projections.
+  Class foo (m : Set) := { pf : m = m }.
+  Notation pf' m := (pf (m:=m)). (* Wrong argument name: m. *)
+End Prim.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/closed/HoTT_coq_083.v
new file mode 100644
index 0000000000..494b25c7b1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_083.v
@@ -0,0 +1,29 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob : Type }.
+
+Goal forall C, ob C -> ob C.
+intros.
+generalize dependent (ob C).
+(* 1 subgoals, subgoal 1 (ID 7)
+
+  C : category
+  ============================
+   forall T : Type, T -> T
+(dependent evars:) *)
+intros T t.
+Undo 2.
+generalize dependent (@ob C).
+(* 1 subgoals, subgoal 1 (ID 6)
+
+  C : category
+  X : ob C
+  ============================
+   Type -> ob C
+(dependent evars:) *)
+intros T t.
+(* Toplevel input, characters 9-10:
+Error: No product even after head-reduction. *)
diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v
new file mode 100644
index 0000000000..04c675563e
--- /dev/null
+++ b/test-suite/success/rewrite_strat.v
@@ -0,0 +1,53 @@
+Require Import Setoid. 
+
+Variable X : Set.
+
+Variable f : X -> X.
+Variable g : X -> X -> X.
+Variable h : nat -> X -> X.
+
+Variable lem0 : forall x, f (f x) = f x.
+Variable lem1 : forall x, g x x = f x.
+Variable lem2 : forall n x, h (S n) x = g (h n x) (h n x).
+Variable lem3 : forall x, h 0 x = x.
+
+Hint Rewrite lem0 lem1 lem2 lem3 : rew.
+
+Goal forall x, h 10 x = f x.
+Proof. 
+  intros.
+  Time autorewrite with rew. (* 0.586 *)
+  reflexivity.
+Time Qed. (* 0.53 *)
+
+Goal forall x, h 6 x = f x.
+intros.
+  Time rewrite_strat topdown lem2.
+  Time rewrite_strat topdown lem1.
+  Time rewrite_strat topdown lem0.
+  Time rewrite_strat topdown lem3.
+  reflexivity.
+Undo 5.
+  Time rewrite_strat topdown (choice lem2 lem1).
+  Time rewrite_strat topdown (choice lem0 lem3).
+  reflexivity.
+Undo 3. 
+  Time rewrite_strat (topdown (choice lem2 lem1); topdown (choice lem0 lem3)).
+  reflexivity.
+Undo 2.
+  Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))). 
+  reflexivity.  
+Undo 2.
+  Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))).
+  reflexivity.
+Qed.
+
+Goal forall x, h 10 x = f x.
+Proof. 
+  intros.
+  Time rewrite_strat topdown (hints rew). (* 0.38 *)
+  reflexivity.
+Time Qed. (* 0.06 s *)
+
+Set Printing All.
+Set Printing Depth 100000.
\ No newline at end of file