← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/bugs/closed/shouldsucceed/1414.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/bugs/closed/shouldsucceed/1414.v
 
1
Require Import ZArith Coq.Program.Wf Coq.Program.Utils.
 
2
 
 
3
Parameter data:Set.
 
4
 
 
5
Inductive t : Set :=
 
6
  | Leaf : t
 
7
  | Node : t -> data -> t -> Z -> t.
 
8
 
 
9
Parameter avl : t -> Prop.
 
10
Parameter bst : t -> Prop. 
 
11
Parameter In : data -> t -> Prop. 
 
12
Parameter cardinal : t -> nat.
 
13
Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
 
14
 
 
15
Parameter split : data -> t -> t*(bool*t).
 
16
Parameter join : t -> data -> t -> t.
 
17
Parameter add : data -> t -> t.
 
18
 
 
19
Program Fixpoint union 
 
20
  (s:t*t)
 
21
  (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) 
 
22
  { measure card2 s } : 
 
23
  {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd
 
24
s)} := 
 
25
  match s with 
 
26
    | (Leaf,t2) => t2
 
27
    | (t1,Leaf) => t1
 
28
    | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) =>        
 
29
        if (Z_ge_lt_dec h1 h2) then
 
30
          if (Z_eq_dec h2 1) 
 
31
          then add v2 (fst s)
 
32
          else
 
33
            let (l2', r2') := split v1 (snd s) in
 
34
            join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _)
 
35
        else
 
36
          if (Z_eq_dec h1 1) 
 
37
          then add v1 (snd s) 
 
38
          else
 
39
            let (l1', r1') := split v2 (fst s) in
 
40
            join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _)
 
41
  end.