1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
new file mode 100644
index 00000000..323021de
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -0,0 +1,20 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+   computed when the user explicitly indicated it *)
+
+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.