diff options
author | 2009-04-14 03:29:03 +0000 | |
---|---|---|
committer | 2009-04-14 03:29:03 +0000 | |
commit | 8c91f2ec3afabc78716ae74550324ca499e5084c (patch) | |
tree | b6c48b0e8128542d8cbf4017731838716e401e1e /test-suite/bugs | |
parent | 0e608025f45c9ffc2573c72e5c23bc183e3ab0b3 (diff) |
Fix and actually beautify the bug script to adapt to the new measure
support in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12082 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1414.v | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index d3c008087..06922e50a 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -17,25 +17,24 @@ Parameter join : t -> data -> t -> t. Parameter add : data -> t -> t. Program Fixpoint union - (s:t*t) - (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) - { measure card2 s } : - {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd -s)} := - match s with - | (Leaf,t2) => t2 - | (t1,Leaf) => t1 - | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) => + (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 + | Leaf,t2 => t2 + | t1,Leaf => t1 + | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then if (Z_eq_dec h2 1) - then add v2 (fst s) + then add v2 s else - let (l2', r2') := split v1 (snd s) in - join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _) + let (l2', r2') := split v1 u in + join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else if (Z_eq_dec h1 1) - then add v1 (snd s) + then add v1 s else - let (l1', r1') := split v2 (fst s) in - join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _) + let (l1', r1') := split v2 u in + join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _) end. |