Correction d'un bug dans check + ajout de tests

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

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
new file mode 100644
index 0000000000..2ac7454b0c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -0,0 +1,29 @@
+Require Import List.
+
+Inductive Tree : Set :=
+| Br : Tree -> Tree -> Tree
+| No : nat -> Tree
+.
+
+(* given a tree, we want to know which lists can
+   be used to navigate exactly to a node *)
+Inductive Exact : Tree -> list bool -> Prop :=
+| exDone  n    :              Exact (No n)   nil
+| exLeft  l r p: Exact l p -> Exact (Br l r) (true::p)
+| exRight l r p: Exact r p -> Exact (Br l r) (false::p)
+.
+
+Definition unreachable A : False -> A.
+intros.
+destruct H.
+Defined.
+
+Program Fixpoint fetch t p (x:Exact t p) {struct x} :=
+   match t, p with
+   | No p' , nil      => p'
+   | No p' , _::_     => unreachable nat _
+   | Br l r, nil      => unreachable nat _ 
+   | Br l r, true::t  => fetch l t _
+   | Br l r, false::t => fetch r t _
+   end.
+