1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/failure/subterm3.v b/test-suite/failure/subterm3.v
new file mode 100644
index 00000000..2cef6357
--- /dev/null
+++ b/test-suite/failure/subterm3.v
@@ -0,0 +1,29 @@
+(* An example showing that prop-extensionality is incompatible with
+   powerful extensions of the guard condition.
+   This is a variation on the example in subterm2, exploiting
+   missing typing constraints in the commutative cut subterm rule
+   (subterm2 is using the same flaw but for the match rule).
+
+   Example due to Cristóbal Camarero on Coq-Club.
+ *)
+
+Axiom prop_ext: forall P Q, (P <-> Q) -> P=Q.
+
+Inductive True2 : Prop := I3 : (False -> True2) -> True2.
+
+Theorem T3T: True2 = True.
+Proof.
+apply prop_ext; split; auto.
+intros; constructor; apply False_rect.
+Qed.
+
+Theorem T3F_FT3F : (True2 -> False) = ((False -> True2) -> False).
+Proof.
+rewrite T3T.
+apply prop_ext; split; auto.
+Qed.
+
+Fail Fixpoint loop (x : True2) : False :=
+match x with
+I3 f => (match T3F_FT3F in _=T return T with eq_refl=> loop end) f
+end.