diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1414.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1414.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index 06922e50a..495a16bca 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -7,8 +7,8 @@ Inductive t : Set := | Node : t -> data -> t -> Z -> t. Parameter avl : t -> Prop. -Parameter bst : t -> Prop. -Parameter In : data -> t -> Prop. +Parameter bst : t -> Prop. +Parameter In : data -> t -> Prop. Parameter cardinal : t -> nat. Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2. @@ -16,25 +16,25 @@ Parameter split : data -> t -> t*(bool*t). Parameter join : t -> data -> t -> t. Parameter add : data -> t -> t. -Program Fixpoint union +Program Fixpoint union (s u:t) - (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) - { measure (cardinal s + cardinal u) } : - {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := - match s, u with + (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) + { measure (cardinal s + cardinal u) } : + {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := + match s, u with | Leaf,t2 => t2 | t1,Leaf => t1 - | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => + | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then - if (Z_eq_dec h2 1) + if (Z_eq_dec h2 1) then add v2 s else let (l2', r2') := split v1 u in join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else - if (Z_eq_dec h1 1) + if (Z_eq_dec h1 1) then add v1 s else let (l1', r1') := split v2 u in join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _) - end. + end. |