Test file for #4695: Slow Qed.

1 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 000000000..a42271811
--- /dev/null
+++ b/test-suite/bugs/closed/4695.v
@@ -0,0 +1,38 @@
+(* 
+The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel
+term comparison after evaluation was done on constants according to their user
+names. The conversion still succeeded because delta applied, but was much
+slower than with a canonical names comparison.
+*)
+
+Module Mod0.
+
+  Fixpoint rec_ t d : nat :=
+    match d with
+    | O => O
+    | S d' =>
+      match t with
+      | true => rec_ t d'
+      | false => rec_ t d'
+      end
+    end.
+
+  Definition depth := 1000.
+
+  Definition rec t := rec_ t depth.
+
+End Mod0.
+
+
+Module Mod1.
+  Module M := Mod0.
+End Mod1.
+
+
+Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n.
+
+Lemma slow_qed : forall t n,
+    Mod0.rec t = n.
+Proof.
+  intros; unfold Mod0.rec; apply rec_prop.
+Timeout 2 Qed.