Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/1939.v b/test-suite/bugs/closed/1939.v
new file mode 100644
index 00000000..5e61529b
--- /dev/null
+++ b/test-suite/bugs/closed/1939.v
@@ -0,0 +1,19 @@
+Require Import Setoid Program.Basics.
+
+ Parameter P : nat -> Prop.
+ Parameter R : nat -> nat -> Prop.
+
+ Add Parametric Morphism : P
+   with signature R ++> impl as PM1.
+ Admitted.
+
+ Add Parametric Morphism : P
+   with signature R --> impl as PM2.
+ Admitted.
+
+ Goal forall x y, R x y -> P y -> P x.
+ Proof.
+   intros x y H1 H2.
+   rewrite H1.
+   auto.
+ Qed.
\ No newline at end of file