Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
new file mode 100644
index 00000000..9629b213
--- /dev/null
+++ b/test-suite/success/rewrite.v
@@ -0,0 +1,19 @@
+(* Check that dependent rewrite applies on arbitrary terms *)
+
+Inductive listn : nat -> Set :=
+  | niln : listn 0
+  | consn : forall n : nat, nat -> listn n -> listn (S n).
+
+Axiom
+  ax :
+    forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
+    existS _ (n + n') l = existS _ (n' + n) l'.
+
+Lemma lem :
+ forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
+ n + n' = n' + n /\ existT _ (n + n') l = existT _ (n' + n) l'.
+Proof.
+intros n n' l l'.
+ dependent rewrite (ax n n' l l').
+split; reflexivity.
+Qed.