From 00a13c3c014e2729d17ad8e8191f20586ae3b52b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 3 May 2016 15:50:13 +0200 Subject: Test file for #4695: Slow Qed. --- test-suite/bugs/closed/4695.v | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test-suite/bugs/closed/4695.v (limited to 'test-suite') 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. -- cgit v1.2.3