2 files changed, 35 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 000000000..323021dea
--- /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.        
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
new file mode 100644
index 000000000..948cea3ee
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -0,0 +1,15 @@
+(* Some check of Miller's pattern inference - used to fail in 8.2 due
+   first to the presence of aliases, secondly due to the absence of
+   restriction of the potential interesting variables to the subset of
+   variables effectively occurring in the term to instantiate *)
+
+Set Implicit Arguments.
+
+Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
+
+Variable H : exists x : bool, True.
+ 
+Definition coef :=
+match Some true	with
+  Some _ => @choose _ H |_ => true 
+end .