From 2fb65d97bfd9ccba49b6081810f1a72841bb3d55 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 5 Feb 2008 10:41:38 +0000
Subject: Ajout d'un test pour le bug #1787

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10507 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/1787.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/1787.v

diff --git a/test-suite/bugs/closed/1787.v b/test-suite/bugs/closed/1787.v
new file mode 100644
index 0000000000..8e1024e6ec
--- /dev/null
+++ b/test-suite/bugs/closed/1787.v
@@ -0,0 +1,11 @@
+Parameter P : nat -> nat -> Prop.
+Parameter Q : nat -> nat -> Prop.
+Axiom A : forall x x' x'', P x x' -> Q x'' x' -> P x x''.
+
+Goal (P 1 3) -> (Q 1 3) -> (P 1 1).
+intros H H'.
+refine ((fun H1 : P 1 _ => let H2 := (_:Q 1 _) in A _ _ _ H1 H2) _).
+clear.
+Admitted.
+
+
-- 
cgit v1.2.3