Ajout d'un test pour le bug #1779

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10468 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1779.v b/test-suite/bugs/closed/shouldsucceed/1779.v
new file mode 100644
index 000000000..95bb66b96
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1779.v
@@ -0,0 +1,25 @@
+Require Import Div2.
+
+Lemma double_div2: forall n, div2 (double n) = n.
+exact (fun n =>  let _subcase :=
+    let _cofact := fun _ : 0 = 0 => refl_equal 0 in
+    _cofact (let _fact := refl_equal 0 in _fact) in
+  let _subcase0 :=
+    fun (m : nat) (Hrec : div2 (double m) = m) =>
+    let _fact := f_equal div2 (double_S m) in
+    let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in
+    let _eq0 :=
+      trans_eq _eq
+        (trans_eq
+           (f_equal (fun f : nat -> nat => f (div2 (double m)))
+              (refl_equal S)) (f_equal S Hrec)) in
+    _eq0 in
+  (fix _fix (__ : nat) : div2 (double __) = __ :=
+     match __ as n return (div2 (double n) = n) with
+     | 0 => _subcase
+     | S __0 =>
+         (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec)
+           (_fix __0)
+     end) n).
+Guarded.
+Defined.