summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2613.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2613.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2613.v17
1 files changed, 0 insertions, 17 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v
deleted file mode 100644
index 4f0470b1..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2613.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* 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.
-