Imported Upstream version 8.5~beta1+dfsg

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2001.v b/test-suite/bugs/closed/2001.v
new file mode 100644
index 00000000..d0b3bf17
--- /dev/null
+++ b/test-suite/bugs/closed/2001.v
@@ -0,0 +1,22 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+   computed when the user explicitly indicated it *)
+
+Unset Automatic Introduction.
+
+Inductive T : Set :=
+| v : T.
+
+Definition f (s:nat) (t:T) : nat.
+fix 2.
+intros s t.
+refine
+  match t with
+  | v => s
+  end.
+Defined.
+
+Lemma test :
+  forall s, f s v = s.
+Proof.
+reflexivity.
+Qed.