Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 17 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 00000000..4f0470b1
--- /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.
+