diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /test-suite/bugs/closed/4695.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'test-suite/bugs/closed/4695.v')
-rw-r--r-- | test-suite/bugs/closed/4695.v | 38 |
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 00000000..a4227181 --- /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. |