aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1411.v
diff options
context:
space:
mode:
authorVincent Laporte2018-10-02 13:44:46 +0000
committerVincent Laporte2018-10-04 08:01:34 +0000
commitdb22ae6140259dd065fdd80af4cb3c3bab41c184 (patch)
treee17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/1411.v
parent53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff)
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/closed/1411.v')
-rw-r--r--test-suite/bugs/closed/1411.v35
1 files changed, 0 insertions, 35 deletions
diff --git a/test-suite/bugs/closed/1411.v b/test-suite/bugs/closed/1411.v
deleted file mode 100644
index a1a7b288a5..0000000000
--- a/test-suite/bugs/closed/1411.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import List.
-Require Import Program.
-
-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 t} :=
- 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.
-
-Next Obligation. inversion x. Qed.
-Next Obligation. inversion x. Qed.
-Next Obligation. inversion x; trivial. Qed.
-Next Obligation. inversion x; trivial. Qed.
-