Regression tests for bugs #2613 and #2616.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14604 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v
new file mode 100644
index 0000000000..4f0470b1df
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2613.v
@@ -0,0 +1,17 @@
+(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
+
+Require Import ZArith.
+Require Recdef.
+
+Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
+
+Locate eq_sym.  (* Constant Coq.Init.Logic.eq_sym  *)
+
+Function loop (n: nat) {measure (fun x => x) n} : bool :=
+  if nat_eq_dec n 0 then false else loop (pred n).
+Proof.
+   admit.
+Defined.
+
+Check eq_sym eq_refl : 0=0.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v
new file mode 100644
index 0000000000..8758e32dd8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2616.v
@@ -0,0 +1,7 @@
+(* Testing ill-typed rewrite which used to succeed in 8.3 *)
+Goal 
+  forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), 
+    N 0 -> False.
+Proof.
+intros.
+Fail rewrite IN in H.