From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2
---
theories/MSets/MSetRBT.v | 1931 ++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 1931 insertions(+)
create mode 100644 theories/MSets/MSetRBT.v
(limited to 'theories/MSets/MSetRBT.v')
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
new file mode 100644
index 00000000..b53c0392
--- /dev/null
+++ b/theories/MSets/MSetRBT.v
@@ -0,0 +1,1931 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* option (elt * t).
+
+ Axiom remove_min_spec1 : forall s k s',
+ remove_min s = Some (k,s') ->
+ min_elt s = Some k /\ remove k s [=] s'.
+
+ Axiom remove_min_spec2 : forall s, remove_min s = None -> Empty s.
+
+End MSetRemoveMin.
+
+(** The type of color annotation. *)
+
+Inductive color := Red | Black.
+
+Module Color.
+ Definition t := color.
+End Color.
+
+(** * Ops : the pure functions *)
+
+Module Ops (X:Orders.OrderedType) <: MSetInterface.Ops X.
+
+(** ** Generic trees instantiated with color *)
+
+(** We reuse a generic definition of trees where the information
+ parameter is a color. Functions like mem or fold are also
+ provided by this generic functor. *)
+
+Include MSetGenTree.Ops X Color.
+
+Definition t := tree.
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+
+(** ** Basic tree *)
+
+Definition singleton (k: elt) : tree := Bk Leaf k Leaf.
+
+(** ** Changing root color *)
+
+Definition makeBlack t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a x b => Bk a x b
+ end.
+
+Definition makeRed t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a x b => Rd a x b
+ end.
+
+(** ** Balancing *)
+
+(** We adapt when one side is not a true red-black tree.
+ Both sides have the same black depth. *)
+
+Definition lbal l k r :=
+ match l with
+ | Rd (Rd a x b) y c => Rd (Bk a x b) y (Bk c k r)
+ | Rd a x (Rd b y c) => Rd (Bk a x b) y (Bk c k r)
+ | _ => Bk l k r
+ end.
+
+Definition rbal l k r :=
+ match r with
+ | Rd (Rd b y c) z d => Rd (Bk l k b) y (Bk c z d)
+ | Rd b y (Rd c z d) => Rd (Bk l k b) y (Bk c z d)
+ | _ => Bk l k r
+ end.
+
+(** A variant of [rbal], with reverse pattern order.
+ Is it really useful ? Should we always use it ? *)
+
+Definition rbal' l k r :=
+ match r with
+ | Rd b y (Rd c z d) => Rd (Bk l k b) y (Bk c z d)
+ | Rd (Rd b y c) z d => Rd (Bk l k b) y (Bk c z d)
+ | _ => Bk l k r
+ end.
+
+(** Balancing with different black depth.
+ One side is almost a red-black tree, while the other is
+ a true red-black tree, but with black depth + 1.
+ Used in deletion. *)
+
+Definition lbalS l k r :=
+ match l with
+ | Rd a x b => Rd (Bk a x b) k r
+ | _ =>
+ match r with
+ | Bk a y b => rbal' l k (Rd a y b)
+ | Rd (Bk a y b) z c => Rd (Bk l k a) y (rbal' b z (makeRed c))
+ | _ => Rd l k r (* impossible *)
+ end
+ end.
+
+Definition rbalS l k r :=
+ match r with
+ | Rd b y c => Rd l k (Bk b y c)
+ | _ =>
+ match l with
+ | Bk a x b => lbal (Rd a x b) k r
+ | Rd a x (Bk b y c) => Rd (lbal (makeRed a) x b) y (Bk c k r)
+ | _ => Rd l k r (* impossible *)
+ end
+ end.
+
+(** ** Insertion *)
+
+Fixpoint ins x s :=
+ match s with
+ | Leaf => Rd Leaf x Leaf
+ | Node c l y r =>
+ match X.compare x y with
+ | Eq => s
+ | Lt =>
+ match c with
+ | Red => Rd (ins x l) y r
+ | Black => lbal (ins x l) y r
+ end
+ | Gt =>
+ match c with
+ | Red => Rd l y (ins x r)
+ | Black => rbal l y (ins x r)
+ end
+ end
+ end.
+
+Definition add x s := makeBlack (ins x s).
+
+(** ** Deletion *)
+
+Fixpoint append (l:tree) : tree -> tree :=
+ match l with
+ | Leaf => fun r => r
+ | Node lc ll lx lr =>
+ fix append_l (r:tree) : tree :=
+ match r with
+ | Leaf => l
+ | Node rc rl rx rr =>
+ match lc, rc with
+ | Red, Red =>
+ let lrl := append lr rl in
+ match lrl with
+ | Rd lr' x rl' => Rd (Rd ll lx lr') x (Rd rl' rx rr)
+ | _ => Rd ll lx (Rd lrl rx rr)
+ end
+ | Black, Black =>
+ let lrl := append lr rl in
+ match lrl with
+ | Rd lr' x rl' => Rd (Bk ll lx lr') x (Bk rl' rx rr)
+ | _ => lbalS ll lx (Bk lrl rx rr)
+ end
+ | Black, Red => Rd (append_l rl) rx rr
+ | Red, Black => Rd ll lx (append lr r)
+ end
+ end
+ end.
+
+Fixpoint del x t :=
+ match t with
+ | Leaf => Leaf
+ | Node _ a y b =>
+ match X.compare x y with
+ | Eq => append a b
+ | Lt =>
+ match a with
+ | Bk _ _ _ => lbalS (del x a) y b
+ | _ => Rd (del x a) y b
+ end
+ | Gt =>
+ match b with
+ | Bk _ _ _ => rbalS a y (del x b)
+ | _ => Rd a y (del x b)
+ end
+ end
+ end.
+
+Definition remove x t := makeBlack (del x t).
+
+(** ** Removing minimal element *)
+
+Fixpoint delmin l x r : (elt * tree) :=
+ match l with
+ | Leaf => (x,r)
+ | Node lc ll lx lr =>
+ let (k,l') := delmin ll lx lr in
+ match lc with
+ | Black => (k, lbalS l' x r)
+ | Red => (k, Rd l' x r)
+ end
+ end.
+
+Definition remove_min t : option (elt * tree) :=
+ match t with
+ | Leaf => None
+ | Node _ l x r =>
+ let (k,t) := delmin l x r in
+ Some (k, makeBlack t)
+ end.
+
+(** ** Tree-ification
+
+ We rebuild a tree of size [if pred then n-1 else n] as soon
+ as the list [l] has enough elements *)
+
+Definition bogus : tree * list elt := (Leaf, nil).
+
+Notation treeify_t := (list elt -> tree * list elt).
+
+Definition treeify_zero : treeify_t :=
+ fun acc => (Leaf,acc).
+
+Definition treeify_one : treeify_t :=
+ fun acc => match acc with
+ | x::acc => (Rd Leaf x Leaf, acc)
+ | _ => bogus
+ end.
+
+Definition treeify_cont (f g : treeify_t) : treeify_t :=
+ fun acc =>
+ match f acc with
+ | (l, x::acc) =>
+ match g acc with
+ | (r, acc) => (Bk l x r, acc)
+ end
+ | _ => bogus
+ end.
+
+Fixpoint treeify_aux (pred:bool)(n: positive) : treeify_t :=
+ match n with
+ | xH => if pred then treeify_zero else treeify_one
+ | xO n => treeify_cont (treeify_aux pred n) (treeify_aux true n)
+ | xI n => treeify_cont (treeify_aux false n) (treeify_aux pred n)
+ end.
+
+Fixpoint plength (l:list elt) := match l with
+ | nil => 1%positive
+ | _::l => Psucc (plength l)
+end.
+
+Definition treeify (l:list elt) :=
+ fst (treeify_aux true (plength l) l).
+
+(** ** Filtering *)
+
+Fixpoint filter_aux (f: elt -> bool) s acc :=
+ match s with
+ | Leaf => acc
+ | Node _ l k r =>
+ let acc := filter_aux f r acc in
+ if f k then filter_aux f l (k::acc)
+ else filter_aux f l acc
+ end.
+
+Definition filter (f: elt -> bool) (s: t) : t :=
+ treeify (filter_aux f s nil).
+
+Fixpoint partition_aux (f: elt -> bool) s acc1 acc2 :=
+ match s with
+ | Leaf => (acc1,acc2)
+ | Node _ sl k sr =>
+ let (acc1, acc2) := partition_aux f sr acc1 acc2 in
+ if f k then partition_aux f sl (k::acc1) acc2
+ else partition_aux f sl acc1 (k::acc2)
+ end.
+
+Definition partition (f: elt -> bool) (s:t) : t*t :=
+ let (ok,ko) := partition_aux f s nil nil in
+ (treeify ok, treeify ko).
+
+(** ** Union, intersection, difference *)
+
+(** union of the elements of [l1] and [l2] into a third [acc] list. *)
+
+Fixpoint union_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => @rev_append _
+ | x::l1' =>
+ fix union_l1 l2 acc :=
+ match l2 with
+ | nil => rev_append l1 acc
+ | y::l2' =>
+ match X.compare x y with
+ | Eq => union_list l1' l2' (x::acc)
+ | Lt => union_l1 l2' (y::acc)
+ | Gt => union_list l1' l2 (x::acc)
+ end
+ end
+ end.
+
+Definition linear_union s1 s2 :=
+ treeify (union_list (rev_elements s1) (rev_elements s2) nil).
+
+Fixpoint inter_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => fun _ acc => acc
+ | x::l1' =>
+ fix inter_l1 l2 acc :=
+ match l2 with
+ | nil => acc
+ | y::l2' =>
+ match X.compare x y with
+ | Eq => inter_list l1' l2' (x::acc)
+ | Lt => inter_l1 l2' acc
+ | Gt => inter_list l1' l2 acc
+ end
+ end
+ end.
+
+Definition linear_inter s1 s2 :=
+ treeify (inter_list (rev_elements s1) (rev_elements s2) nil).
+
+Fixpoint diff_list l1 : list elt -> list elt -> list elt :=
+ match l1 with
+ | nil => fun _ acc => acc
+ | x::l1' =>
+ fix diff_l1 l2 acc :=
+ match l2 with
+ | nil => rev_append l1 acc
+ | y::l2' =>
+ match X.compare x y with
+ | Eq => diff_list l1' l2' acc
+ | Lt => diff_l1 l2' acc
+ | Gt => diff_list l1' l2 (x::acc)
+ end
+ end
+ end.
+
+Definition linear_diff s1 s2 :=
+ treeify (diff_list (rev_elements s1) (rev_elements s2) nil).
+
+(** [compare_height] returns:
+ - [Lt] if [height s2] is at least twice [height s1];
+ - [Gt] if [height s1] is at least twice [height s2];
+ - [Eq] if heights are approximately equal.
+ Warning: this is not an equivalence relation! but who cares.... *)
+
+Definition skip_red t :=
+ match t with
+ | Rd t' _ _ => t'
+ | _ => t
+ end.
+
+Definition skip_black t :=
+ match skip_red t with
+ | Bk t' _ _ => t'
+ | t' => t'
+ end.
+
+Fixpoint compare_height (s1x s1 s2 s2x: tree) : comparison :=
+ match skip_red s1x, skip_red s1, skip_red s2, skip_red s2x with
+ | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
+ compare_height (skip_black s2x') s1' s2' (skip_black s2x')
+ | _, Leaf, _, Node _ _ _ _ => Lt
+ | Node _ _ _ _, _, Leaf, _ => Gt
+ | Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Leaf =>
+ compare_height (skip_black s1x') s1' s2' Leaf
+ | Leaf, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
+ compare_height Leaf s1' s2' (skip_black s2x')
+ | _, _, _, _ => Eq
+ end.
+
+(** When one tree is quite smaller than the other, we simply
+ adds repeatively all its elements in the big one.
+ For trees of comparable height, we rather use [linear_union]. *)
+
+Definition union (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => fold add t1 t2
+ | Gt => fold add t2 t1
+ | Eq => linear_union t1 t2
+ end.
+
+Definition diff (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => filter (fun k => negb (mem k t2)) t1
+ | Gt => fold remove t2 t1
+ | Eq => linear_diff t1 t2
+ end.
+
+Definition inter (t1 t2: t) : t :=
+ match compare_height t1 t1 t2 t2 with
+ | Lt => filter (fun k => mem k t2) t1
+ | Gt => filter (fun k => mem k t1) t2
+ | Eq => linear_inter t1 t2
+ end.
+
+End Ops.
+
+(** * MakeRaw : the pure functions and their specifications *)
+
+Module Type MakeRaw (X:Orders.OrderedType) <: MSetInterface.RawSets X.
+Include Ops X.
+
+(** Generic definition of binary-search-trees and proofs of
+ specifications for generic functions such as mem or fold. *)
+
+Include MSetGenTree.Props X Color.
+
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+
+Local Hint Immediate MX.eq_sym.
+Local Hint Unfold In lt_tree gt_tree Ok.
+Local Hint Constructors InT bst.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Local Hint Resolve elements_spec2.
+
+(** ** Singleton set *)
+
+Lemma singleton_spec x y : InT y (singleton x) <-> X.eq y x.
+Proof.
+ unfold singleton; intuition_in.
+Qed.
+
+Instance singleton_ok x : Ok (singleton x).
+Proof.
+ unfold singleton; auto.
+Qed.
+
+(** ** makeBlack, MakeRed *)
+
+Lemma makeBlack_spec s x : InT x (makeBlack s) <-> InT x s.
+Proof.
+ destruct s; simpl; intuition_in.
+Qed.
+
+Lemma makeRed_spec s x : InT x (makeRed s) <-> InT x s.
+Proof.
+ destruct s; simpl; intuition_in.
+Qed.
+
+Instance makeBlack_ok s `{Ok s} : Ok (makeBlack s).
+Proof.
+ destruct s; simpl; ok.
+Qed.
+
+Instance makeRed_ok s `{Ok s} : Ok (makeRed s).
+Proof.
+ destruct s; simpl; ok.
+Qed.
+
+(** ** Generic handling for red-matching and red-red-matching *)
+
+Definition isblack t :=
+ match t with Bk _ _ _ => True | _ => False end.
+
+Definition notblack t :=
+ match t with Bk _ _ _ => False | _ => True end.
+
+Definition notred t :=
+ match t with Rd _ _ _ => False | _ => True end.
+
+Definition rcase {A} f g t : A :=
+ match t with
+ | Rd a x b => f a x b
+ | _ => g t
+ end.
+
+Inductive rspec {A} f g : tree -> A -> Prop :=
+ | rred a x b : rspec f g (Rd a x b) (f a x b)
+ | relse t : notred t -> rspec f g t (g t).
+
+Fact rmatch {A} f g t : rspec (A:=A) f g t (rcase f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; now constructor.
+Qed.
+
+Definition rrcase {A} f g t : A :=
+ match t with
+ | Rd (Rd a x b) y c => f a x b y c
+ | Rd a x (Rd b y c) => f a x b y c
+ | _ => g t
+ end.
+
+Notation notredred := (rrcase (fun _ _ _ _ _ => False) (fun _ => True)).
+
+Inductive rrspec {A} f g : tree -> A -> Prop :=
+ | rrleft a x b y c : rrspec f g (Rd (Rd a x b) y c) (f a x b y c)
+ | rrright a x b y c : rrspec f g (Rd a x (Rd b y c)) (f a x b y c)
+ | rrelse t : notredred t -> rrspec f g t (g t).
+
+Fact rrmatch {A} f g t : rrspec (A:=A) f g t (rrcase f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; try now constructor.
+destruct l as [|[|] ll lx lr], r as [|[|] rl rx rr]; now constructor.
+Qed.
+
+Definition rrcase' {A} f g t : A :=
+ match t with
+ | Rd a x (Rd b y c) => f a x b y c
+ | Rd (Rd a x b) y c => f a x b y c
+ | _ => g t
+ end.
+
+Fact rrmatch' {A} f g t : rrspec (A:=A) f g t (rrcase' f g t).
+Proof.
+destruct t as [|[|] l x r]; simpl; try now constructor.
+destruct l as [|[|] ll lx lr], r as [|[|] rl rx rr]; now constructor.
+Qed.
+
+(** Balancing operations are instances of generic match *)
+
+Fact lbal_match l k r :
+ rrspec
+ (fun a x b y c => Rd (Bk a x b) y (Bk c k r))
+ (fun l => Bk l k r)
+ l
+ (lbal l k r).
+Proof.
+ exact (rrmatch _ _ _).
+Qed.
+
+Fact rbal_match l k r :
+ rrspec
+ (fun a x b y c => Rd (Bk l k a) x (Bk b y c))
+ (fun r => Bk l k r)
+ r
+ (rbal l k r).
+Proof.
+ exact (rrmatch _ _ _).
+Qed.
+
+Fact rbal'_match l k r :
+ rrspec
+ (fun a x b y c => Rd (Bk l k a) x (Bk b y c))
+ (fun r => Bk l k r)
+ r
+ (rbal' l k r).
+Proof.
+ exact (rrmatch' _ _ _).
+Qed.
+
+Fact lbalS_match l x r :
+ rspec
+ (fun a y b => Rd (Bk a y b) x r)
+ (fun l =>
+ match r with
+ | Bk a y b => rbal' l x (Rd a y b)
+ | Rd (Bk a y b) z c => Rd (Bk l x a) y (rbal' b z (makeRed c))
+ | _ => Rd l x r
+ end)
+ l
+ (lbalS l x r).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Fact rbalS_match l x r :
+ rspec
+ (fun a y b => Rd l x (Bk a y b))
+ (fun r =>
+ match l with
+ | Bk a y b => lbal (Rd a y b) x r
+ | Rd a y (Bk b z c) => Rd (lbal (makeRed a) y b) z (Bk c x r)
+ | _ => Rd l x r
+ end)
+ r
+ (rbalS l x r).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+(** ** Balancing for insertion *)
+
+Lemma lbal_spec l x r y :
+ InT y (lbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case lbal_match; intuition_in.
+Qed.
+
+Instance lbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (lbal l x r).
+Proof.
+ destruct (lbal_match l x r); ok.
+Qed.
+
+Lemma rbal_spec l x r y :
+ InT y (rbal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbal_match; intuition_in.
+Qed.
+
+Instance rbal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (rbal l x r).
+Proof.
+ destruct (rbal_match l x r); ok.
+Qed.
+
+Lemma rbal'_spec l x r y :
+ InT y (rbal' l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbal'_match; intuition_in.
+Qed.
+
+Instance rbal'_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+ Ok (rbal' l x r).
+Proof.
+ destruct (rbal'_match l x r); ok.
+Qed.
+
+Hint Rewrite In_node_iff In_leaf_iff
+ makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb.
+
+Ltac descolor := destruct_all Color.t.
+Ltac destree t := destruct t as [|[|] ? ? ?].
+Ltac autorew := autorewrite with rb.
+Tactic Notation "autorew" "in" ident(H) := autorewrite with rb in H.
+
+(** ** Insertion *)
+
+Lemma ins_spec : forall s x y,
+ InT y (ins x s) <-> X.eq y x \/ InT y s.
+Proof.
+ induct s x.
+ - intuition_in.
+ - intuition_in. setoid_replace y with x; eauto.
+ - descolor; autorew; rewrite IHl; intuition_in.
+ - descolor; autorew; rewrite IHr; intuition_in.
+Qed.
+Hint Rewrite ins_spec : rb.
+
+Instance ins_ok s x `{Ok s} : Ok (ins x s).
+Proof.
+ induct s x; auto; descolor;
+ (apply lbal_ok || apply rbal_ok || ok); auto;
+ intros y; autorew; intuition; order.
+Qed.
+
+Lemma add_spec' s x y :
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof.
+ unfold add. now autorew.
+Qed.
+
+Hint Rewrite add_spec' : rb.
+
+Lemma add_spec s x y `{Ok s} :
+ InT y (add x s) <-> X.eq y x \/ InT y s.
+Proof.
+ apply add_spec'.
+Qed.
+
+Instance add_ok s x `{Ok s} : Ok (add x s).
+Proof.
+ unfold add; auto_tc.
+Qed.
+
+(** ** Balancing for deletion *)
+
+Lemma lbalS_spec l x r y :
+ InT y (lbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case lbalS_match.
+ - intros; autorew; intuition_in.
+ - clear l. intros l _.
+ destruct r as [|[|] rl rx rr].
+ * autorew. intuition_in.
+ * destree rl; autorew; intuition_in.
+ * autorew. intuition_in.
+Qed.
+
+Instance lbalS_ok l x r :
+ forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (lbalS l x r).
+Proof.
+ case lbalS_match; intros.
+ - ok.
+ - destruct r as [|[|] rl rx rr].
+ * ok.
+ * destruct rl as [|[|] rll rlx rlr]; intros; ok.
+ + apply rbal'_ok; ok.
+ intros w; autorew; auto.
+ + intros w; autorew.
+ destruct 1 as [Hw|[Hw|Hw]]; try rewrite Hw; eauto.
+ * ok. autorew. apply rbal'_ok; ok.
+Qed.
+
+Lemma rbalS_spec l x r y :
+ InT y (rbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
+Proof.
+ case rbalS_match.
+ - intros; autorew; intuition_in.
+ - intros t _.
+ destruct l as [|[|] ll lx lr].
+ * autorew. intuition_in.
+ * destruct lr as [|[|] lrl lrx lrr]; autorew; intuition_in.
+ * autorew. intuition_in.
+Qed.
+
+Instance rbalS_ok l x r :
+ forall `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (rbalS l x r).
+Proof.
+ case rbalS_match; intros.
+ - ok.
+ - destruct l as [|[|] ll lx lr].
+ * ok.
+ * destruct lr as [|[|] lrl lrx lrr]; intros; ok.
+ + apply lbal_ok; ok.
+ intros w; autorew; auto.
+ + intros w; autorew.
+ destruct 1 as [Hw|[Hw|Hw]]; try rewrite Hw; eauto.
+ * ok. apply lbal_ok; ok.
+Qed.
+
+Hint Rewrite lbalS_spec rbalS_spec : rb.
+
+(** ** Append for deletion *)
+
+Ltac append_tac l r :=
+ induction l as [| lc ll _ lx lr IHlr];
+ [intro r; simpl
+ |induction r as [| rc rl IHrl rx rr _];
+ [simpl
+ |destruct lc, rc;
+ [specialize (IHlr rl); clear IHrl
+ |simpl;
+ assert (Hr:notred (Bk rl rx rr)) by (simpl; trivial);
+ set (r:=Bk rl rx rr) in *; clearbody r; clear IHrl rl rx rr;
+ specialize (IHlr r)
+ |change (append _ _) with (Rd (append (Bk ll lx lr) rl) rx rr);
+ assert (Hl:notred (Bk ll lx lr)) by (simpl; trivial);
+ set (l:=Bk ll lx lr) in *; clearbody l; clear IHlr ll lx lr
+ |specialize (IHlr rl); clear IHrl]]].
+
+Fact append_rr_match ll lx lr rl rx rr :
+ rspec
+ (fun a x b => Rd (Rd ll lx a) x (Rd b rx rr))
+ (fun t => Rd ll lx (Rd t rx rr))
+ (append lr rl)
+ (append (Rd ll lx lr) (Rd rl rx rr)).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Fact append_bb_match ll lx lr rl rx rr :
+ rspec
+ (fun a x b => Rd (Bk ll lx a) x (Bk b rx rr))
+ (fun t => lbalS ll lx (Bk t rx rr))
+ (append lr rl)
+ (append (Bk ll lx lr) (Bk rl rx rr)).
+Proof.
+ exact (rmatch _ _ _).
+Qed.
+
+Lemma append_spec l r x :
+ InT x (append l r) <-> InT x l \/ InT x r.
+Proof.
+ revert r.
+ append_tac l r; autorew; try tauto.
+ - (* Red / Red *)
+ revert IHlr; case append_rr_match;
+ [intros a y b | intros t Ht]; autorew; tauto.
+ - (* Black / Black *)
+ revert IHlr; case append_bb_match;
+ [intros a y b | intros t Ht]; autorew; tauto.
+Qed.
+
+Hint Rewrite append_spec : rb.
+
+Lemma append_ok : forall x l r `{Ok l, Ok r},
+ lt_tree x l -> gt_tree x r -> Ok (append l r).
+Proof.
+ append_tac l r.
+ - (* Leaf / _ *)
+ trivial.
+ - (* _ / Leaf *)
+ trivial.
+ - (* Red / Red *)
+ intros; inv.
+ assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr.
+ assert (X.lt lx rx) by (transitivity x; eauto).
+ assert (G : gt_tree lx (append lr rl)).
+ { intros w. autorew. destruct 1; [|transitivity x]; eauto. }
+ assert (L : lt_tree rx (append lr rl)).
+ { intros w. autorew. destruct 1; [transitivity x|]; eauto. }
+ revert IH G L; case append_rr_match; intros; ok.
+ - (* Red / Black *)
+ intros; ok.
+ intros w; autorew; destruct 1; eauto.
+ - (* Black / Red *)
+ intros; ok.
+ intros w; autorew; destruct 1; eauto.
+ - (* Black / Black *)
+ intros; inv.
+ assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr.
+ assert (X.lt lx rx) by (transitivity x; eauto).
+ assert (G : gt_tree lx (append lr rl)).
+ { intros w. autorew. destruct 1; [|transitivity x]; eauto. }
+ assert (L : lt_tree rx (append lr rl)).
+ { intros w. autorew. destruct 1; [transitivity x|]; eauto. }
+ revert IH G L; case append_bb_match; intros; ok.
+ apply lbalS_ok; ok.
+Qed.
+
+(** ** Deletion *)
+
+Lemma del_spec : forall s x y `{Ok s},
+ InT y (del x s) <-> InT y s /\ ~X.eq y x.
+Proof.
+induct s x.
+- intuition_in.
+- autorew; intuition_in.
+ assert (X.lt y x') by eauto. order.
+ assert (X.lt x' y) by eauto. order.
+ order.
+- destruct l as [|[|] ll lx lr]; autorew;
+ rewrite ?IHl by trivial; intuition_in; order.
+- destruct r as [|[|] rl rx rr]; autorew;
+ rewrite ?IHr by trivial; intuition_in; order.
+Qed.
+
+Hint Rewrite del_spec : rb.
+
+Instance del_ok s x `{Ok s} : Ok (del x s).
+Proof.
+induct s x.
+- trivial.
+- eapply append_ok; eauto.
+- assert (lt_tree x' (del x l)).
+ { intro w. autorew; trivial. destruct 1. eauto. }
+ destruct l as [|[|] ll lx lr]; auto_tc.
+- assert (gt_tree x' (del x r)).
+ { intro w. autorew; trivial. destruct 1. eauto. }
+ destruct r as [|[|] rl rx rr]; auto_tc.
+Qed.
+
+Lemma remove_spec s x y `{Ok s} :
+ InT y (remove x s) <-> InT y s /\ ~X.eq y x.
+Proof.
+unfold remove. now autorew.
+Qed.
+
+Hint Rewrite remove_spec : rb.
+
+Instance remove_ok s x `{Ok s} : Ok (remove x s).
+Proof.
+unfold remove; auto_tc.
+Qed.
+
+(** ** Removing the minimal element *)
+
+Lemma delmin_spec l y r c x s' `{O : Ok (Node c l y r)} :
+ delmin l y r = (x,s') ->
+ min_elt (Node c l y r) = Some x /\ del x (Node c l y r) = s'.
+Proof.
+ revert y r c x s' O.
+ induction l as [|lc ll IH ly lr _].
+ - simpl. intros y r _ x s' _. injection 1; intros; subst.
+ now rewrite MX.compare_refl.
+ - intros y r c x s' O.
+ simpl delmin.
+ specialize (IH ly lr). destruct delmin as (x0,s0).
+ destruct (IH lc x0 s0); clear IH; [ok|trivial|].
+ remember (Node lc ll ly lr) as l.
+ simpl min_elt in *.
+ intros E.
+ replace x0 with x in * by (destruct lc; now injection E).
+ split.
+ * subst l; intuition.
+ * assert (X.lt x y).
+ { inversion_clear O.
+ assert (InT x l) by now apply min_elt_spec1. auto. }
+ simpl. case X.compare_spec; try order.
+ destruct lc; injection E; clear E; intros; subst l s0; auto.
+Qed.
+
+Lemma remove_min_spec1 s x s' `{Ok s}:
+ remove_min s = Some (x,s') ->
+ min_elt s = Some x /\ remove x s = s'.
+Proof.
+ unfold remove_min.
+ destruct s as [|c l y r]; try easy.
+ generalize (delmin_spec l y r c).
+ destruct delmin as (x0,s0). intros D.
+ destruct (D x0 s0) as (->,<-); auto.
+ fold (remove x0 (Node c l y r)).
+ inversion_clear 1; auto.
+Qed.
+
+Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
+Proof.
+ unfold remove_min.
+ destruct s as [|c l y r].
+ - easy.
+ - now destruct delmin.
+Qed.
+
+Lemma remove_min_ok (s:t) `{Ok s}:
+ match remove_min s with
+ | Some (_,s') => Ok s'
+ | None => True
+ end.
+Proof.
+ generalize (remove_min_spec1 s).
+ destruct remove_min as [(x0,s0)|]; auto.
+ intros R. destruct (R x0 s0); auto. subst s0. auto_tc.
+Qed.
+
+(** ** Treeify *)
+
+Notation ifpred p n := (if p then pred n else n%nat).
+
+Definition treeify_invariant size (f:treeify_t) :=
+ forall acc,
+ size <= length acc ->
+ let (t,acc') := f acc in
+ cardinal t = size /\ acc = elements t ++ acc'.
+
+Lemma treeify_zero_spec : treeify_invariant 0 treeify_zero.
+Proof.
+ intro. simpl. auto.
+Qed.
+
+Lemma treeify_one_spec : treeify_invariant 1 treeify_one.
+Proof.
+ intros [|x acc]; simpl; auto; inversion 1.
+Qed.
+
+Lemma treeify_cont_spec f g size1 size2 size :
+ treeify_invariant size1 f ->
+ treeify_invariant size2 g ->
+ size = S (size1 + size2) ->
+ treeify_invariant size (treeify_cont f g).
+Proof.
+ intros Hf Hg EQ acc LE. unfold treeify_cont.
+ specialize (Hf acc).
+ destruct (f acc) as (t1,acc1).
+ destruct Hf as (Hf1,Hf2).
+ { lia. }
+ destruct acc1 as [|x acc1].
+ { exfalso. subst acc.
+ rewrite <- app_nil_end, <- elements_cardinal in LE. lia. }
+ specialize (Hg acc1).
+ destruct (g acc1) as (t2,acc2).
+ destruct Hg as (Hg1,Hg2).
+ { subst acc. rewrite app_length, <- elements_cardinal in LE.
+ simpl in LE. unfold elt in *. lia. }
+ simpl. split.
+ * lia.
+ * rewrite elements_node, app_ass. simpl. unfold elt in *; congruence.
+Qed.
+
+Lemma treeify_aux_spec n (p:bool) :
+ treeify_invariant (ifpred p (Pos.to_nat n)) (treeify_aux p n).
+Proof.
+ revert p.
+ induction n as [n|n|]; intros p; simpl treeify_aux.
+ - eapply treeify_cont_spec; [ apply (IHn false) | apply (IHn p) | ].
+ rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
+ destruct p; simpl; lia.
+ - eapply treeify_cont_spec; [ apply (IHn p) | apply (IHn true) | ].
+ rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
+ destruct p; simpl; lia.
+ - destruct p; [ apply treeify_zero_spec | apply treeify_one_spec ].
+Qed.
+
+Lemma plength_spec l : Pos.to_nat (plength l) = S (length l).
+Proof.
+ induction l; simpl; now rewrite ?Pos2Nat.inj_succ, ?IHl.
+Qed.
+
+Lemma treeify_elements l : elements (treeify l) = l.
+Proof.
+ assert (H := treeify_aux_spec (plength l) true l).
+ unfold treeify. destruct treeify_aux as (t,acc); simpl in *.
+ destruct H as (H,H'). { now rewrite plength_spec. }
+ subst l. rewrite plength_spec, app_length, <- elements_cardinal in *.
+ destruct acc.
+ * now rewrite app_nil_r.
+ * simpl in H. lia.
+Qed.
+
+Lemma treeify_spec x l : InT x (treeify l) <-> InA X.eq x l.
+Proof.
+ intros. now rewrite <- elements_spec1, treeify_elements.
+Qed.
+
+Lemma treeify_ok l : sort X.lt l -> Ok (treeify l).
+Proof.
+ intros. apply elements_sort_ok. rewrite treeify_elements; auto.
+Qed.
+
+
+(** ** Filter *)
+
+Lemma filter_app A f (l l':list A) :
+ List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
+Proof.
+ induction l as [|x l IH]; simpl; trivial.
+ destruct (f x); simpl; now rewrite IH.
+Qed.
+
+Lemma filter_aux_elements s f acc :
+ filter_aux f s acc = List.filter f (elements s) ++ acc.
+Proof.
+ revert acc.
+ induction s as [|c l IHl x r IHr]; simpl; trivial.
+ intros acc.
+ rewrite elements_node, filter_app. simpl.
+ destruct (f x); now rewrite IHl, IHr, app_ass.
+Qed.
+
+Lemma filter_elements s f :
+ elements (filter f s) = List.filter f (elements s).
+Proof.
+ unfold filter.
+ now rewrite treeify_elements, filter_aux_elements, app_nil_r.
+Qed.
+
+Lemma filter_spec s x f :
+ Proper (X.eq==>Logic.eq) f ->
+ (InT x (filter f s) <-> InT x s /\ f x = true).
+Proof.
+ intros Hf.
+ rewrite <- elements_spec1, filter_elements, filter_InA, elements_spec1;
+ now auto_tc.
+Qed.
+
+Instance filter_ok s f `(Ok s) : Ok (filter f s).
+Proof.
+ apply elements_sort_ok.
+ rewrite filter_elements.
+ apply filter_sort with X.eq; auto_tc.
+Qed.
+
+(** ** Partition *)
+
+Lemma partition_aux_spec s f acc1 acc2 :
+ partition_aux f s acc1 acc2 =
+ (filter_aux f s acc1, filter_aux (fun x => negb (f x)) s acc2).
+Proof.
+ revert acc1 acc2.
+ induction s as [ | c l Hl x r Hr ]; simpl.
+ - trivial.
+ - intros acc1 acc2.
+ destruct (f x); simpl; now rewrite Hr, Hl.
+Qed.
+
+Lemma partition_spec s f :
+ partition f s = (filter f s, filter (fun x => negb (f x)) s).
+Proof.
+ unfold partition, filter. now rewrite partition_aux_spec.
+Qed.
+
+Lemma partition_spec1 s f :
+ Proper (X.eq==>Logic.eq) f ->
+ Equal (fst (partition f s)) (filter f s).
+Proof. now rewrite partition_spec. Qed.
+
+Lemma partition_spec2 s f :
+ Proper (X.eq==>Logic.eq) f ->
+ Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+Proof. now rewrite partition_spec. Qed.
+
+Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+Proof. rewrite partition_spec; now apply filter_ok. Qed.
+
+Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+Proof. rewrite partition_spec; now apply filter_ok. Qed.
+
+
+(** ** An invariant for binary list functions with accumulator. *)
+
+Ltac inA :=
+ rewrite ?InA_app_iff, ?InA_cons, ?InA_nil, ?InA_rev in *; auto_tc.
+
+Record INV l1 l2 acc : Prop := {
+ l1_sorted : sort X.lt (rev l1);
+ l2_sorted : sort X.lt (rev l2);
+ acc_sorted : sort X.lt acc;
+ l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y;
+ l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}.
+Local Hint Resolve l1_sorted l2_sorted acc_sorted.
+
+Lemma INV_init s1 s2 `(Ok s1, Ok s2) :
+ INV (rev_elements s1) (rev_elements s2) nil.
+Proof.
+ rewrite !rev_elements_rev.
+ split; rewrite ?rev_involutive; auto; intros; now inA.
+Qed.
+
+Lemma INV_sym l1 l2 acc : INV l1 l2 acc -> INV l2 l1 acc.
+Proof.
+ destruct 1; now split.
+Qed.
+
+Lemma INV_drop x1 l1 l2 acc :
+ INV (x1 :: l1) l2 acc -> INV l1 l2 acc.
+Proof.
+ intros (l1s,l2s,accs,l1a,l2a). simpl in *.
+ destruct (sorted_app_inv _ _ l1s) as (U & V & W); auto.
+ split; auto.
+Qed.
+
+Lemma INV_eq x1 x2 l1 l2 acc :
+ INV (x1 :: l1) (x2 :: l2) acc -> X.eq x1 x2 ->
+ INV l1 l2 (x1 :: acc).
+Proof.
+ intros (U,V,W,X,Y) EQ. simpl in *.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ split; auto.
+ - constructor; auto. apply InA_InfA with X.eq; auto_tc.
+ - intros x y; inA; intros Hx [Hy|Hy].
+ + apply U3; inA.
+ + apply X; inA.
+ - intros x y; inA; intros Hx [Hy|Hy].
+ + rewrite Hy, EQ; apply V3; inA.
+ + apply Y; inA.
+Qed.
+
+Lemma INV_lt x1 x2 l1 l2 acc :
+ INV (x1 :: l1) (x2 :: l2) acc -> X.lt x1 x2 ->
+ INV (x1 :: l1) l2 (x2 :: acc).
+Proof.
+ intros (U,V,W,X,Y) EQ. simpl in *.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ split; auto.
+ - constructor; auto. apply InA_InfA with X.eq; auto_tc.
+ - intros x y; inA; intros Hx [Hy|Hy].
+ + rewrite Hy; clear Hy. destruct Hx; [order|].
+ transitivity x1; auto. apply U3; inA.
+ + apply X; inA.
+ - intros x y; inA; intros Hx [Hy|Hy].
+ + rewrite Hy. apply V3; inA.
+ + apply Y; inA.
+Qed.
+
+Lemma INV_rev l1 l2 acc :
+ INV l1 l2 acc -> Sorted X.lt (rev_append l1 acc).
+Proof.
+ intros. rewrite rev_append_rev.
+ apply SortA_app with X.eq; eauto with *.
+ intros x y. inA. eapply l1_lt_acc; eauto.
+Qed.
+
+(** ** union *)
+
+Lemma union_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (union_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1];
+ [intro l2|induction l2 as [|x2 l2 IH2]];
+ intros acc inv.
+ - eapply INV_rev, INV_sym; eauto.
+ - eapply INV_rev; eauto.
+ - simpl. case X.compare_spec; intro C.
+ * apply IH1. eapply INV_eq; eauto.
+ * apply (IH2 (x2::acc)). eapply INV_lt; eauto.
+ * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.
+Qed.
+
+Instance linear_union_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_union s1 s2).
+Proof.
+ unfold linear_union. now apply treeify_ok, union_list_ok, INV_init.
+Qed.
+
+Instance fold_add_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (fold add s1 s2).
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
+Proof.
+ unfold union. destruct compare_height; auto_tc.
+Qed.
+
+Lemma union_list_spec x l1 l2 acc :
+ InA X.eq x (union_list l1 l2 acc) <->
+ InA X.eq x l1 \/ InA X.eq x l2 \/ InA X.eq x acc.
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. rewrite rev_append_rev. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc; simpl.
+ * rewrite rev_append_rev. inA. tauto.
+ * case X.compare_spec; intro C.
+ + rewrite IH1, !InA_cons, C; tauto.
+ + rewrite (IH2 (x2::acc)), !InA_cons. tauto.
+ + rewrite IH1, !InA_cons; tauto.
+Qed.
+
+Lemma linear_union_spec s1 s2 x :
+ InT x (linear_union s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ unfold linear_union.
+ rewrite treeify_spec, union_list_spec, !rev_elements_rev.
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc.
+ tauto.
+Qed.
+
+Lemma fold_add_spec s1 s2 x :
+ InT x (fold add s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl.
+ - rewrite InA_nil. tauto.
+ - unfold flip. rewrite add_spec', IHl, InA_cons. tauto.
+Qed.
+
+Lemma union_spec' s1 s2 x :
+ InT x (union s1 s2) <-> InT x s1 \/ InT x s2.
+Proof.
+ unfold union. destruct compare_height.
+ - apply linear_union_spec.
+ - apply fold_add_spec.
+ - rewrite fold_add_spec. tauto.
+Qed.
+
+Lemma union_spec : forall s1 s2 y `{Ok s1, Ok s2},
+ (InT y (union s1 s2) <-> InT y s1 \/ InT y s2).
+Proof.
+ intros; apply union_spec'.
+Qed.
+
+(** ** inter *)
+
+Lemma inter_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (inter_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1]; [|induction l2 as [|x2 l2 IH2]]; simpl.
+ - eauto.
+ - eauto.
+ - intros acc inv.
+ case X.compare_spec; intro C.
+ * apply IH1. eapply INV_eq; eauto.
+ * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto.
+ * apply IH1. eapply INV_drop; eauto.
+Qed.
+
+Instance linear_inter_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_inter s1 s2).
+Proof.
+ unfold linear_inter. now apply treeify_ok, inter_list_ok, INV_init.
+Qed.
+
+Instance inter_ok s1 s2 `(Ok s1, Ok s2) : Ok (inter s1 s2).
+Proof.
+ unfold inter. destruct compare_height; auto_tc.
+Qed.
+
+Lemma inter_list_spec x l1 l2 acc :
+ sort X.lt (rev l1) ->
+ sort X.lt (rev l2) ->
+ (InA X.eq x (inter_list l1 l2 acc) <->
+ (InA X.eq x l1 /\ InA X.eq x l2) \/ InA X.eq x acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc.
+ * simpl. inA. tauto.
+ * simpl. intros U V.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ case X.compare_spec; intro C.
+ + rewrite IH1, !InA_cons, C; tauto.
+ + rewrite (IH2 acc); auto. inA. intuition; try order.
+ assert (X.lt x x1) by (apply U3; inA). order.
+ + rewrite IH1; auto. inA. intuition; try order.
+ assert (X.lt x x2) by (apply V3; inA). order.
+Qed.
+
+Lemma linear_inter_spec s1 s2 x `(Ok s1, Ok s2) :
+ InT x (linear_inter s1 s2) <-> InT x s1 /\ InT x s2.
+Proof.
+ unfold linear_inter.
+ rewrite !rev_elements_rev, treeify_spec, inter_list_spec
+ by (rewrite rev_involutive; auto_tc).
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.
+Qed.
+
+Local Instance mem_proper s `(Ok s) :
+ Proper (X.eq ==> Logic.eq) (fun k => mem k s).
+Proof.
+ intros x y EQ. apply Bool.eq_iff_eq_true; rewrite !mem_spec; auto.
+ now rewrite EQ.
+Qed.
+
+Lemma inter_spec s1 s2 y `{Ok s1, Ok s2} :
+ InT y (inter s1 s2) <-> InT y s1 /\ InT y s2.
+Proof.
+ unfold inter. destruct compare_height.
+ - now apply linear_inter_spec.
+ - rewrite filter_spec, mem_spec by auto_tc; tauto.
+ - rewrite filter_spec, mem_spec by auto_tc; tauto.
+Qed.
+
+(** ** difference *)
+
+Lemma diff_list_ok l1 l2 acc :
+ INV l1 l2 acc -> sort X.lt (diff_list l1 l2 acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1];
+ [intro l2|induction l2 as [|x2 l2 IH2]];
+ intros acc inv.
+ - eauto.
+ - unfold diff_list. eapply INV_rev; eauto.
+ - simpl. case X.compare_spec; intro C.
+ * apply IH1. eapply INV_drop, INV_sym, INV_drop, INV_sym; eauto.
+ * apply (IH2 acc). eapply INV_sym, INV_drop, INV_sym; eauto.
+ * apply IH1. eapply INV_sym, INV_lt; eauto. now apply INV_sym.
+Qed.
+
+Instance diff_inter_ok s1 s2 `(Ok s1, Ok s2) :
+ Ok (linear_diff s1 s2).
+Proof.
+ unfold linear_inter. now apply treeify_ok, diff_list_ok, INV_init.
+Qed.
+
+Instance fold_remove_ok s1 s2 `(Ok s2) :
+ Ok (fold remove s1 s2).
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance diff_ok s1 s2 `(Ok s1, Ok s2) : Ok (diff s1 s2).
+Proof.
+ unfold diff. destruct compare_height; auto_tc.
+Qed.
+
+Lemma diff_list_spec x l1 l2 acc :
+ sort X.lt (rev l1) ->
+ sort X.lt (rev l2) ->
+ (InA X.eq x (diff_list l1 l2 acc) <->
+ (InA X.eq x l1 /\ ~InA X.eq x l2) \/ InA X.eq x acc).
+Proof.
+ revert l2 acc.
+ induction l1 as [|x1 l1 IH1].
+ - intros l2 acc; simpl. inA. tauto.
+ - induction l2 as [|x2 l2 IH2]; intros acc.
+ * intros; simpl. rewrite rev_append_rev. inA. tauto.
+ * simpl. intros U V.
+ destruct (sorted_app_inv _ _ U) as (U1 & U2 & U3); auto.
+ destruct (sorted_app_inv _ _ V) as (V1 & V2 & V3); auto.
+ case X.compare_spec; intro C.
+ + rewrite IH1; auto. f_equiv. inA. intuition; try order.
+ assert (X.lt x x1) by (apply U3; inA). order.
+ + rewrite (IH2 acc); auto. f_equiv. inA. intuition; try order.
+ assert (X.lt x x1) by (apply U3; inA). order.
+ + rewrite IH1; auto. inA. intuition; try order.
+ left; split; auto. destruct 1. order.
+ assert (X.lt x x2) by (apply V3; inA). order.
+Qed.
+
+Lemma linear_diff_spec s1 s2 x `(Ok s1, Ok s2) :
+ InT x (linear_diff s1 s2) <-> InT x s1 /\ ~InT x s2.
+Proof.
+ unfold linear_diff.
+ rewrite !rev_elements_rev, treeify_spec, diff_list_spec
+ by (rewrite rev_involutive; auto_tc).
+ rewrite !InA_rev, InA_nil, !elements_spec1 by auto_tc. tauto.
+Qed.
+
+Lemma fold_remove_spec s1 s2 x `(Ok s2) :
+ InT x (fold remove s1 s2) <-> InT x s2 /\ ~InT x s1.
+Proof.
+ rewrite fold_spec, <- fold_left_rev_right.
+ rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc.
+ unfold elt in *.
+ induction (rev (elements s1)); simpl; intros.
+ - rewrite InA_nil. intuition.
+ - unfold flip in *. rewrite remove_spec, IHl, InA_cons. tauto.
+ clear IHl. induction l; simpl; auto_tc.
+Qed.
+
+Lemma diff_spec s1 s2 y `{Ok s1, Ok s2} :
+ InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2.
+Proof.
+ unfold diff. destruct compare_height.
+ - now apply linear_diff_spec.
+ - rewrite filter_spec, Bool.negb_true_iff,
+ <- Bool.not_true_iff_false, mem_spec;
+ intuition.
+ intros x1 x2 EQ. f_equal. now apply mem_proper.
+ - now apply fold_remove_spec.
+Qed.
+
+End MakeRaw.
+
+(** * Balancing properties
+
+ We now prove that all operations preserve a red-black invariant,
+ and that trees have hence a logarithmic depth.
+*)
+
+Module BalanceProps(X:Orders.OrderedType)(Import M : MakeRaw X).
+
+Local Notation Rd := (Node Red).
+Local Notation Bk := (Node Black).
+Import M.MX.
+
+(** ** Red-Black invariants *)
+
+(** In a red-black tree :
+ - a red node has no red children
+ - the black depth at each node is the same along all paths.
+ The black depth is here an argument of the predicate. *)
+
+Inductive rbt : nat -> tree -> Prop :=
+ | RB_Leaf : rbt 0 Leaf
+ | RB_Rd n l k r :
+ notred l -> notred r -> rbt n l -> rbt n r -> rbt n (Rd l k r)
+ | RB_Bk n l k r : rbt n l -> rbt n r -> rbt (S n) (Bk l k r).
+
+(** A red-red tree is almost a red-black tree, except that it has
+ a _red_ root node which _may_ have red children. Note that a
+ red-red tree is hence non-empty, and all its strict subtrees
+ are red-black. *)
+
+Inductive rrt (n:nat) : tree -> Prop :=
+ | RR_Rd l k r : rbt n l -> rbt n r -> rrt n (Rd l k r).
+
+(** An almost-red-black tree is almost a red-black tree, except that
+ it's permitted to have two red nodes in a row at the very root (only).
+ We implement this notion by saying that a quasi-red-black tree
+ is either a red-black tree or a red-red tree. *)
+
+Inductive arbt (n:nat)(t:tree) : Prop :=
+ | ARB_RB : rbt n t -> arbt n t
+ | ARB_RR : rrt n t -> arbt n t.
+
+(** The main exported invariant : being a red-black tree for some
+ black depth. *)
+
+Class Rbt (t:tree) := RBT : exists d, rbt d t.
+
+(** ** Basic tactics and results about red-black *)
+
+Scheme rbt_ind := Induction for rbt Sort Prop.
+Local Hint Constructors rbt rrt arbt.
+Local Hint Extern 0 (notred _) => (exact I).
+Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction.
+Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end.
+Ltac nonzero n := destruct n as [|n]; [try split; invrb|].
+
+Lemma rr_nrr_rb n t :
+ rrt n t -> notredred t -> rbt n t.
+Proof.
+ destruct 1 as [l x r Hl Hr].
+ destruct l, r; descolor; invrb; auto.
+Qed.
+
+Local Hint Resolve rr_nrr_rb.
+
+Lemma arb_nrr_rb n t :
+ arbt n t -> notredred t -> rbt n t.
+Proof.
+ destruct 1; auto.
+Qed.
+
+Lemma arb_nr_rb n t :
+ arbt n t -> notred t -> rbt n t.
+Proof.
+ destruct 1; destruct t; descolor; invrb; auto.
+Qed.
+
+Local Hint Resolve arb_nrr_rb arb_nr_rb.
+
+(** ** A Red-Black tree has indeed a logarithmic depth *)
+
+Definition redcarac s := rcase (fun _ _ _ => 1) (fun _ => 0) s.
+
+Lemma rb_maxdepth s n : rbt n s -> maxdepth s <= 2*n + redcarac s.
+Proof.
+ induction 1.
+ - simpl; auto.
+ - replace (redcarac l) with 0 in * by now destree l.
+ replace (redcarac r) with 0 in * by now destree r.
+ simpl maxdepth. simpl redcarac.
+ rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
+ now apply Nat.max_lub.
+ - simpl. Nat.nzsimpl. rewrite <- Nat.succ_le_mono.
+ apply Nat.max_lub; eapply Nat.le_trans; eauto.
+ destree l; simpl; lia.
+ destree r; simpl; lia.
+Qed.
+
+Lemma rb_mindepth s n : rbt n s -> n + redcarac s <= mindepth s.
+Proof.
+ induction 1; simpl.
+ - trivial.
+ - rewrite Nat.add_succ_r.
+ apply -> Nat.succ_le_mono.
+ replace (redcarac l) with 0 in * by now destree l.
+ replace (redcarac r) with 0 in * by now destree r.
+ now apply Nat.min_glb.
+ - apply -> Nat.succ_le_mono. apply Nat.min_glb; lia.
+Qed.
+
+Lemma maxdepth_upperbound s : Rbt s ->
+ maxdepth s <= 2 * log2 (S (cardinal s)).
+Proof.
+ intros (n,H).
+ eapply Nat.le_trans; [eapply rb_maxdepth; eauto|].
+ generalize (rb_mindepth s n H).
+ generalize (mindepth_log_cardinal s). lia.
+Qed.
+
+Lemma maxdepth_lowerbound s : s<>Leaf ->
+ log2 (cardinal s) < maxdepth s.
+Proof.
+ apply maxdepth_log_cardinal.
+Qed.
+
+
+(** ** Singleton *)
+
+Lemma singleton_rb x : Rbt (singleton x).
+Proof.
+ unfold singleton. exists 1; auto.
+Qed.
+
+(** ** [makeBlack] and [makeRed] *)
+
+Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
+Proof.
+ destruct t as [|[|] l x r].
+ - exists 0; auto.
+ - destruct 1; invrb; exists (S n); simpl; auto.
+ - exists n; auto.
+Qed.
+
+Lemma makeRed_rr t n :
+ rbt (S n) t -> notred t -> rrt n (makeRed t).
+Proof.
+ destruct t as [|[|] l x r]; invrb; simpl; auto.
+Qed.
+
+(** ** Balancing *)
+
+Lemma lbal_rb n l k r :
+ arbt n l -> rbt n r -> rbt (S n) (lbal l k r).
+Proof.
+case lbal_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma rbal_rb n l k r :
+ rbt n l -> arbt n r -> rbt (S n) (rbal l k r).
+Proof.
+case rbal_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma rbal'_rb n l k r :
+ rbt n l -> arbt n r -> rbt (S n) (rbal' l k r).
+Proof.
+case rbal'_match; intros; desarb; invrb; auto.
+Qed.
+
+Lemma lbalS_rb n l x r :
+ arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x r).
+Proof.
+ intros Hl Hr Hr'.
+ destruct r as [|[|] rl rx rr]; invrb. clear Hr'.
+ revert Hl.
+ case lbalS_match.
+ - destruct 1; invrb; auto.
+ - intros. apply rbal'_rb; auto.
+Qed.
+
+Lemma lbalS_arb n l x r :
+ arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x r).
+Proof.
+ case lbalS_match.
+ - destruct 1; invrb; auto.
+ - clear l. intros l Hl Hl' Hr.
+ destruct r as [|[|] rl rx rr]; invrb.
+ * destruct rl as [|[|] rll rlx rlr]; invrb.
+ right; auto using rbal'_rb, makeRed_rr.
+ * left; apply rbal'_rb; auto.
+Qed.
+
+Lemma rbalS_rb n l x r :
+ rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x r).
+Proof.
+ intros Hl Hl' Hr.
+ destruct l as [|[|] ll lx lr]; invrb. clear Hl'.
+ revert Hr.
+ case rbalS_match.
+ - destruct 1; invrb; auto.
+ - intros. apply lbal_rb; auto.
+Qed.
+
+Lemma rbalS_arb n l x r :
+ rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x r).
+Proof.
+ case rbalS_match.
+ - destruct 2; invrb; auto.
+ - clear r. intros r Hr Hr' Hl.
+ destruct l as [|[|] ll lx lr]; invrb.
+ * destruct lr as [|[|] lrl lrx lrr]; invrb.
+ right; auto using lbal_rb, makeRed_rr.
+ * left; apply lbal_rb; auto.
+Qed.
+
+
+(** ** Insertion *)
+
+(** The next lemmas combine simultaneous results about rbt and arbt.
+ A first solution here: statement with [if ... then ... else] *)
+
+Definition ifred s (A B:Prop) := rcase (fun _ _ _ => A) (fun _ => B) s.
+
+Lemma ifred_notred s A B : notred s -> (ifred s A B <-> B).
+Proof.
+ destruct s; descolor; simpl; intuition.
+Qed.
+
+Lemma ifred_or s A B : ifred s A B -> A\/B.
+Proof.
+ destruct s; descolor; simpl; intuition.
+Qed.
+
+Lemma ins_rr_rb x s n : rbt n s ->
+ ifred s (rrt n (ins x s)) (rbt n (ins x s)).
+Proof.
+induction 1 as [ | n l k r | n l k r Hl IHl Hr IHr ].
+- simpl; auto.
+- simpl. rewrite ifred_notred in * by trivial.
+ elim_compare x k; auto.
+- rewrite ifred_notred by trivial.
+ unfold ins; fold ins. (* simpl is too much here ... *)
+ elim_compare x k.
+ * auto.
+ * apply lbal_rb; trivial. apply ifred_or in IHl; intuition.
+ * apply rbal_rb; trivial. apply ifred_or in IHr; intuition.
+Qed.
+
+Lemma ins_arb x s n : rbt n s -> arbt n (ins x s).
+Proof.
+ intros H. apply (ins_rr_rb x), ifred_or in H. intuition.
+Qed.
+
+Instance add_rb x s : Rbt s -> Rbt (add x s).
+Proof.
+ intros (n,H). unfold add. now apply (makeBlack_rb n), ins_arb.
+Qed.
+
+(** ** Deletion *)
+
+(** A second approach here: statement with ... /\ ... *)
+
+Lemma append_arb_rb n l r : rbt n l -> rbt n r ->
+ (arbt n (append l r)) /\
+ (notred l -> notred r -> rbt n (append l r)).
+Proof.
+revert r n.
+append_tac l r.
+- split; auto.
+- split; auto.
+- (* Red / Red *)
+ intros n. invrb.
+ case (IHlr n); auto; clear IHlr.
+ case append_rr_match.
+ + intros a x b _ H; split; invrb.
+ assert (rbt n (Rd a x b)) by auto. invrb. auto.
+ + split; invrb; auto.
+- (* Red / Black *)
+ split; invrb. destruct (IHlr n) as (_,IH); auto.
+- (* Black / Red *)
+ split; invrb. destruct (IHrl n) as (_,IH); auto.
+- (* Black / Black *)
+ nonzero n.
+ invrb.
+ destruct (IHlr n) as (IH,_); auto; clear IHlr.
+ revert IH.
+ case append_bb_match.
+ + intros a x b IH; split; destruct IH; invrb; auto.
+ + split; [left | invrb]; auto using lbalS_rb.
+Qed.
+
+(** A third approach : Lemma ... with ... *)
+
+Lemma del_arb s x n : rbt (S n) s -> isblack s -> arbt n (del x s)
+with del_rb s x n : rbt n s -> notblack s -> rbt n (del x s).
+Proof.
+{ revert n.
+ induct s x; try destruct c; try contradiction; invrb.
+ - apply append_arb_rb; assumption.
+ - assert (IHl' := del_rb l x). clear IHr del_arb del_rb.
+ destruct l as [|[|] ll lx lr]; auto.
+ nonzero n. apply lbalS_arb; auto.
+ - assert (IHr' := del_rb r x). clear IHl del_arb del_rb.
+ destruct r as [|[|] rl rx rr]; auto.
+ nonzero n. apply rbalS_arb; auto. }
+{ revert n.
+ induct s x; try assumption; try destruct c; try contradiction; invrb.
+ - apply append_arb_rb; assumption.
+ - assert (IHl' := del_arb l x). clear IHr del_arb del_rb.
+ destruct l as [|[|] ll lx lr]; auto.
+ nonzero n. destruct n as [|n]; [invrb|]; apply lbalS_rb; auto.
+ - assert (IHr' := del_arb r x). clear IHl del_arb del_rb.
+ destruct r as [|[|] rl rx rr]; auto.
+ nonzero n. apply rbalS_rb; auto. }
+Qed.
+
+Instance remove_rb s x : Rbt s -> Rbt (remove x s).
+Proof.
+ intros (n,H). unfold remove.
+ destruct s as [|[|] l y r].
+ - apply (makeBlack_rb n). auto.
+ - apply (makeBlack_rb n). left. apply del_rb; simpl; auto.
+ - nonzero n. apply (makeBlack_rb n). apply del_arb; simpl; auto.
+Qed.
+
+(** ** Treeify *)
+
+Definition treeify_rb_invariant size depth (f:treeify_t) :=
+ forall acc,
+ size <= length acc ->
+ rbt depth (fst (f acc)) /\
+ size + length (snd (f acc)) = length acc.
+
+Lemma treeify_zero_rb : treeify_rb_invariant 0 0 treeify_zero.
+Proof.
+ intros acc _; simpl; auto.
+Qed.
+
+Lemma treeify_one_rb : treeify_rb_invariant 1 0 treeify_one.
+Proof.
+ intros [|x acc]; simpl; auto; inversion 1.
+Qed.
+
+Lemma treeify_cont_rb f g size1 size2 size d :
+ treeify_rb_invariant size1 d f ->
+ treeify_rb_invariant size2 d g ->
+ size = S (size1 + size2) ->
+ treeify_rb_invariant size (S d) (treeify_cont f g).
+Proof.
+ intros Hf Hg H acc Hacc.
+ unfold treeify_cont.
+ specialize (Hf acc).
+ destruct (f acc) as (l, acc1). simpl in *.
+ destruct Hf as (Hf1, Hf2). { lia. }
+ destruct acc1 as [|x acc2]; simpl in *. { lia. }
+ specialize (Hg acc2).
+ destruct (g acc2) as (r, acc3). simpl in *.
+ destruct Hg as (Hg1, Hg2). { lia. }
+ split; [auto | lia].
+Qed.
+
+Lemma treeify_aux_rb n :
+ exists d, forall (b:bool),
+ treeify_rb_invariant (ifpred b (Pos.to_nat n)) d (treeify_aux b n).
+Proof.
+ induction n as [n (d,IHn)|n (d,IHn)| ].
+ - exists (S d). intros b.
+ eapply treeify_cont_rb; [ apply (IHn false) | apply (IHn b) | ].
+ rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
+ destruct b; simpl; lia.
+ - exists (S d). intros b.
+ eapply treeify_cont_rb; [ apply (IHn b) | apply (IHn true) | ].
+ rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
+ destruct b; simpl; lia.
+ - exists 0; destruct b;
+ [ apply treeify_zero_rb | apply treeify_one_rb ].
+Qed.
+
+(** The black depth of [treeify l] is actually a log2, but
+ we don't need to mention that. *)
+
+Instance treeify_rb l : Rbt (treeify l).
+Proof.
+ unfold treeify.
+ destruct (treeify_aux_rb (plength l)) as (d,H).
+ exists d.
+ apply H.
+ now rewrite plength_spec.
+Qed.
+
+(** ** Filtering *)
+
+Instance filter_rb f s : Rbt (filter f s).
+Proof.
+ unfold filter; auto_tc.
+Qed.
+
+Instance partition_rb1 f s : Rbt (fst (partition f s)).
+Proof.
+ unfold partition. destruct partition_aux. simpl. auto_tc.
+Qed.
+
+Instance partition_rb2 f s : Rbt (snd (partition f s)).
+Proof.
+ unfold partition. destruct partition_aux. simpl. auto_tc.
+Qed.
+
+(** ** Union, intersection, difference *)
+
+Instance fold_add_rb s1 s2 : Rbt s2 -> Rbt (fold add s1 s2).
+Proof.
+ intros. rewrite fold_spec, <- fold_left_rev_right. unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Instance fold_remove_rb s1 s2 : Rbt s2 -> Rbt (fold remove s1 s2).
+Proof.
+ intros. rewrite fold_spec, <- fold_left_rev_right. unfold elt in *.
+ induction (rev (elements s1)); simpl; unfold flip in *; auto_tc.
+Qed.
+
+Lemma union_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (union s1 s2).
+Proof.
+ intros. unfold union, linear_union. destruct compare_height; auto_tc.
+Qed.
+
+Lemma inter_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (inter s1 s2).
+Proof.
+ intros. unfold inter, linear_inter. destruct compare_height; auto_tc.
+Qed.
+
+Lemma diff_rb s1 s2 : Rbt s1 -> Rbt s2 -> Rbt (diff s1 s2).
+Proof.
+ intros. unfold diff, linear_diff. destruct compare_height; auto_tc.
+Qed.
+
+End BalanceProps.
+
+(** * Final Encapsulation
+
+ Now, in order to really provide a functor implementing [S], we
+ need to encapsulate everything into a type of binary search trees.
+ They also happen to be well-balanced, but this has no influence
+ on the correctness of operations, so we won't state this here,
+ see [BalanceProps] if you need more than just the MSet interface.
+*)
+
+Module Type MSetInterface_S_Ext := MSetInterface.S <+ MSetRemoveMin.
+
+Module Make (X: Orders.OrderedType) <:
+ MSetInterface_S_Ext with Module E := X.
+ Module Raw. Include MakeRaw X. End Raw.
+ Include MSetInterface.Raw2Sets X Raw.
+
+ Definition opt_ok (x:option (elt * Raw.t)) :=
+ match x with Some (_,s) => Raw.Ok s | None => True end.
+
+ Definition mk_opt_t (x: option (elt * Raw.t))(P: opt_ok x) :
+ option (elt * t) :=
+ match x as o return opt_ok o -> option (elt * t) with
+ | Some (k,s') => fun P : Raw.Ok s' => Some (k, Mkt s')
+ | None => fun _ => None
+ end P.
+
+ Definition remove_min s : option (elt * t) :=
+ mk_opt_t (Raw.remove_min (this s)) (Raw.remove_min_ok s).
+
+ Lemma remove_min_spec1 s x s' :
+ remove_min s = Some (x,s') ->
+ min_elt s = Some x /\ Equal (remove x s) s'.
+ Proof.
+ destruct s as (s,Hs).
+ unfold remove_min, mk_opt_t, min_elt, remove, Equal, In; simpl.
+ generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
+ set (P := Raw.remove_min_ok s). clearbody P.
+ destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
+ intros H U. injection U. clear U; intros; subst. simpl.
+ destruct (H x s0); auto. subst; intuition.
+ Qed.
+
+ Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
+ Proof.
+ destruct s as (s,Hs).
+ unfold remove_min, mk_opt_t, Empty, In; simpl.
+ generalize (Raw.remove_min_spec2 s).
+ set (P := Raw.remove_min_ok s). clearbody P.
+ destruct (Raw.remove_min s) as [(x0,s0)|]; now intuition.
+ Qed.
+
+End Make.
--
cgit v1.2.3
From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg
---
.gitignore | 5 +-
CHANGES | 166 +-
COMPATIBILITY | 47 +-
INSTALL | 2 +-
INSTALL.macosx | 20 -
Makefile | 36 +-
Makefile.build | 33 +-
Makefile.common | 23 +-
TODO | 53 +
checker/check.ml | 2 +-
checker/check_stat.ml | 2 +-
checker/check_stat.mli | 2 +-
checker/checker.ml | 2 +-
checker/closure.ml | 2 +-
checker/closure.mli | 2 +-
checker/indtypes.ml | 2 +-
checker/indtypes.mli | 2 +-
checker/inductive.ml | 2 +-
checker/inductive.mli | 2 +-
checker/mod_checking.mli | 2 +-
checker/modops.ml | 2 +-
checker/modops.mli | 2 +-
checker/reduction.ml | 2 +-
checker/reduction.mli | 2 +-
checker/safe_typing.ml | 2 +-
checker/safe_typing.mli | 2 +-
checker/subtyping.ml | 2 +-
checker/subtyping.mli | 2 +-
checker/term.ml | 2 +-
checker/type_errors.ml | 2 +-
checker/type_errors.mli | 2 +-
checker/typeops.ml | 2 +-
checker/typeops.mli | 2 +-
checker/validate.ml | 2 +-
config/Makefile.template | 154 --
config/coq_config.mli | 2 +-
configure | 478 ++---
dev/db_printers.ml | 2 +-
dev/header | 2 +-
dev/macosify_accel.sh | 3 +
dev/top_printers.ml | 4 +-
doc/refman/RefMan-sch.tex | 418 -----
doc/stdlib/index-list.html.template | 6 +
ide/command_windows.ml | 2 +-
ide/command_windows.mli | 2 +-
ide/config_lexer.mll | 2 +-
ide/coq.ml | 2 +-
ide/coq.mli | 2 +-
ide/coq_commands.ml | 2 +-
ide/coq_lex.mll | 2 +-
ide/coqide.ml | 13 +-
ide/coqide.mli | 2 +-
ide/coqide_main.ml4 | 2 +-
ide/gtk_parsing.ml | 2 +-
ide/ide_mac_stubs.c | 10 +-
ide/ideproof.ml | 40 +-
ide/ideutils.ml | 2 +-
ide/ideutils.mli | 2 +-
ide/mac_default_accel_map | 726 ++++----
ide/minilib.ml | 55 +-
ide/preferences.ml | 4 +-
ide/preferences.mli | 2 +-
ide/project_file.ml4 | 2 +-
ide/tags.ml | 2 +-
ide/tags.mli | 2 +-
ide/typed_notebook.ml | 2 +-
ide/undo.ml | 2 +-
ide/undo_lablgtk_ge212.mli | 2 +-
ide/undo_lablgtk_ge26.mli | 2 +-
ide/undo_lablgtk_lt26.mli | 2 +-
ide/utf8_convert.mll | 2 +-
interp/constrextern.ml | 58 +-
interp/constrextern.mli | 4 +-
interp/constrintern.ml | 31 +-
interp/constrintern.mli | 2 +-
interp/coqlib.ml | 2 +-
interp/coqlib.mli | 2 +-
interp/dumpglob.ml | 2 +-
interp/dumpglob.mli | 2 +-
interp/genarg.ml | 2 +-
interp/genarg.mli | 2 +-
interp/implicit_quantifiers.ml | 2 +-
interp/implicit_quantifiers.mli | 2 +-
interp/modintern.ml | 2 +-
interp/modintern.mli | 2 +-
interp/notation.ml | 35 +-
interp/notation.mli | 2 +-
interp/ppextend.ml | 2 +-
interp/ppextend.mli | 2 +-
interp/reserve.ml | 2 +-
interp/reserve.mli | 2 +-
interp/smartlocate.ml | 2 +-
interp/smartlocate.mli | 2 +-
interp/syntax_def.ml | 66 +-
interp/syntax_def.mli | 12 +-
interp/topconstr.ml | 2 +-
interp/topconstr.mli | 2 +-
kernel/cbytecodes.ml | 2 +-
kernel/cbytecodes.mli | 4 +-
kernel/cbytegen.ml | 2 +-
kernel/cemitcodes.ml | 2 +-
kernel/closure.ml | 2 +-
kernel/closure.mli | 2 +-
kernel/conv_oracle.ml | 2 +-
kernel/conv_oracle.mli | 2 +-
kernel/cooking.ml | 8 +-
kernel/cooking.mli | 5 +-
kernel/csymtable.ml | 2 +-
kernel/csymtable.mli | 4 +-
kernel/declarations.ml | 2 +-
kernel/declarations.mli | 2 +-
kernel/entries.ml | 2 +-
kernel/entries.mli | 2 +-
kernel/environ.ml | 2 +-
kernel/environ.mli | 2 +-
kernel/esubst.ml | 2 +-
kernel/esubst.mli | 2 +-
kernel/indtypes.ml | 2 +-
kernel/indtypes.mli | 2 +-
kernel/inductive.ml | 2 +-
kernel/inductive.mli | 2 +-
kernel/mod_subst.ml | 2 +-
kernel/mod_subst.mli | 2 +-
kernel/mod_typing.ml | 2 +-
kernel/mod_typing.mli | 2 +-
kernel/modops.ml | 2 +-
kernel/modops.mli | 2 +-
kernel/names.ml | 2 +-
kernel/names.mli | 2 +-
kernel/pre_env.ml | 2 +-
kernel/pre_env.mli | 2 +-
kernel/reduction.ml | 2 +-
kernel/reduction.mli | 2 +-
kernel/retroknowledge.ml | 2 +-
kernel/retroknowledge.mli | 2 +-
kernel/safe_typing.ml | 2 +-
kernel/safe_typing.mli | 2 +-
kernel/sign.ml | 2 +-
kernel/sign.mli | 2 +-
kernel/subtyping.ml | 2 +-
kernel/subtyping.mli | 2 +-
kernel/term.ml | 3 +-
kernel/term.mli | 3 +-
kernel/term_typing.ml | 5 +-
kernel/term_typing.mli | 2 +-
kernel/type_errors.ml | 2 +-
kernel/type_errors.mli | 2 +-
kernel/typeops.ml | 2 +-
kernel/typeops.mli | 2 +-
kernel/univ.ml | 2 +-
kernel/univ.mli | 2 +-
kernel/vconv.mli | 2 +-
kernel/vm.ml | 2 +-
lib/bigint.ml | 355 ++--
lib/bigint.mli | 11 +-
lib/compat.ml4 | 2 +-
lib/dnet.ml | 2 +-
lib/dnet.mli | 2 +-
lib/dyn.ml | 2 +-
lib/dyn.mli | 2 +-
lib/envars.ml | 10 +-
lib/envars.mli | 2 +-
lib/explore.ml | 2 +-
lib/explore.mli | 2 +-
lib/flags.ml | 17 +-
lib/flags.mli | 7 +-
lib/gmap.ml | 2 +-
lib/gmap.mli | 2 +-
lib/gmapl.ml | 2 +-
lib/gmapl.mli | 2 +-
lib/hashcons.ml | 2 +-
lib/hashcons.mli | 2 +-
lib/hashtbl_alt.ml | 2 +-
lib/hashtbl_alt.mli | 2 +-
lib/heap.ml | 2 +-
lib/heap.mli | 2 +-
lib/option.ml | 2 +-
lib/option.mli | 2 +-
lib/pp.ml4 | 13 +-
lib/pp.mli | 6 +-
lib/pp_control.ml | 2 +-
lib/pp_control.mli | 2 +-
lib/profile.ml | 2 +-
lib/profile.mli | 2 +-
lib/rtree.ml | 2 +-
lib/rtree.mli | 2 +-
lib/system.ml | 2 +-
lib/system.mli | 2 +-
lib/tries.ml | 2 +-
lib/unionfind.ml | 2 +-
lib/unionfind.mli | 2 +-
lib/util.mli | 2 +-
lib/xml_lexer.mll | 6 +
library/assumptions.ml | 2 +-
library/assumptions.mli | 2 +-
library/decl_kinds.ml | 2 +-
library/decl_kinds.mli | 2 +-
library/declare.ml | 2 +-
library/declare.mli | 2 +-
library/declaremods.ml | 2 +-
library/declaremods.mli | 2 +-
library/decls.ml | 2 +-
library/decls.mli | 2 +-
library/dischargedhypsmap.ml | 2 +-
library/dischargedhypsmap.mli | 2 +-
library/global.ml | 2 +-
library/global.mli | 2 +-
library/goptions.ml | 2 +-
library/goptions.mli | 2 +-
library/goptionstyp.mli | 2 +-
library/heads.ml | 2 +-
library/heads.mli | 2 +-
library/impargs.ml | 2 +-
library/impargs.mli | 2 +-
library/lib.ml | 2 +-
library/lib.mli | 2 +-
library/libnames.ml | 2 +-
library/libnames.mli | 2 +-
library/libobject.ml | 2 +-
library/libobject.mli | 2 +-
library/library.ml | 2 +-
library/library.mli | 2 +-
library/nameops.ml | 2 +-
library/nameops.mli | 2 +-
library/nametab.ml | 2 +-
library/nametab.mli | 2 +-
library/states.ml | 2 +-
library/states.mli | 2 +-
library/summary.ml | 2 +-
library/summary.mli | 2 +-
parsing/argextend.ml4 | 2 +-
parsing/egrammar.ml | 2 +-
parsing/egrammar.mli | 2 +-
parsing/extend.ml | 2 +-
parsing/extend.mli | 2 +-
parsing/extrawit.ml | 2 +-
parsing/extrawit.mli | 2 +-
parsing/g_constr.ml4 | 2 +-
parsing/g_ltac.ml4 | 3 +-
parsing/g_prim.ml4 | 2 +-
parsing/g_proofs.ml4 | 2 +-
parsing/g_tactic.ml4 | 58 +-
parsing/g_vernac.ml4 | 19 +-
parsing/g_xml.ml4 | 2 +-
parsing/lexer.ml4 | 2 +-
parsing/lexer.mli | 2 +-
parsing/pcoq.ml4 | 2 +-
parsing/pcoq.mli | 2 +-
parsing/ppconstr.ml | 30 +-
parsing/ppconstr.mli | 9 +-
parsing/pptactic.ml | 31 +-
parsing/pptactic.mli | 2 +-
parsing/ppvernac.ml | 22 +-
parsing/ppvernac.mli | 4 +-
parsing/prettyp.ml | 14 +-
parsing/prettyp.mli | 2 +-
parsing/printer.ml | 119 +-
parsing/printer.mli | 6 +-
parsing/printmod.ml | 6 +-
parsing/printmod.mli | 2 +-
parsing/q_constr.ml4 | 2 +-
parsing/q_coqast.ml4 | 24 +-
parsing/q_util.ml4 | 2 +-
parsing/q_util.mli | 2 +-
parsing/tacextend.ml4 | 8 +-
parsing/tactic_printer.ml | 2 +-
parsing/tactic_printer.mli | 2 +-
parsing/tok.ml | 2 +-
parsing/tok.mli | 2 +-
parsing/vernacextend.ml4 | 13 +-
plugins/cc/ccalgo.ml | 2 +-
plugins/cc/ccalgo.mli | 2 +-
plugins/cc/ccproof.ml | 2 +-
plugins/cc/ccproof.mli | 2 +-
plugins/cc/cctac.ml | 8 +-
plugins/cc/cctac.mli | 2 +-
plugins/cc/g_congruence.ml4 | 2 +-
plugins/decl_mode/decl_expr.mli | 2 +-
plugins/decl_mode/decl_interp.ml | 2 +-
plugins/decl_mode/decl_interp.mli | 2 +-
plugins/decl_mode/decl_mode.ml | 2 +-
plugins/decl_mode/decl_mode.mli | 2 +-
plugins/decl_mode/decl_proof_instr.ml | 2 +-
plugins/decl_mode/decl_proof_instr.mli | 2 +-
plugins/decl_mode/g_decl_mode.ml4 | 2 +-
plugins/decl_mode/ppdecl_proof.ml | 2 +-
plugins/extraction/ExtrOcamlBasic.v | 2 +-
plugins/extraction/ExtrOcamlBigIntConv.v | 2 +-
plugins/extraction/ExtrOcamlIntConv.v | 2 +-
plugins/extraction/ExtrOcamlNatBigInt.v | 2 +-
plugins/extraction/ExtrOcamlNatInt.v | 2 +-
plugins/extraction/ExtrOcamlString.v | 2 +-
plugins/extraction/ExtrOcamlZBigInt.v | 8 +-
plugins/extraction/ExtrOcamlZInt.v | 4 +-
plugins/extraction/big.ml | 2 +-
plugins/extraction/common.ml | 4 +-
plugins/extraction/common.mli | 2 +-
plugins/extraction/extract_env.ml | 6 +-
plugins/extraction/extract_env.mli | 2 +-
plugins/extraction/extraction.ml | 2 +-
plugins/extraction/extraction.mli | 2 +-
plugins/extraction/g_extraction.ml4 | 2 +-
plugins/extraction/haskell.ml | 2 +-
plugins/extraction/haskell.mli | 2 +-
plugins/extraction/miniml.mli | 2 +-
plugins/extraction/mlutil.ml | 2 +-
plugins/extraction/mlutil.mli | 2 +-
plugins/extraction/modutil.ml | 2 +-
plugins/extraction/modutil.mli | 2 +-
plugins/extraction/ocaml.ml | 2 +-
plugins/extraction/ocaml.mli | 2 +-
plugins/extraction/scheme.ml | 2 +-
plugins/extraction/scheme.mli | 2 +-
plugins/extraction/table.ml | 3 +-
plugins/extraction/table.mli | 2 +-
plugins/field/LegacyField.v | 2 +-
plugins/field/LegacyField_Compl.v | 2 +-
plugins/field/LegacyField_Tactic.v | 22 +-
plugins/field/LegacyField_Theory.v | 182 +-
plugins/field/field.ml4 | 2 +-
plugins/firstorder/formula.ml | 2 +-
plugins/firstorder/formula.mli | 2 +-
plugins/firstorder/g_ground.ml4 | 2 +-
plugins/firstorder/ground.ml | 2 +-
plugins/firstorder/ground.mli | 2 +-
plugins/firstorder/instances.ml | 2 +-
plugins/firstorder/instances.mli | 2 +-
plugins/firstorder/rules.ml | 2 +-
plugins/firstorder/rules.mli | 2 +-
plugins/firstorder/sequent.ml | 2 +-
plugins/firstorder/sequent.mli | 2 +-
plugins/firstorder/unify.ml | 2 +-
plugins/firstorder/unify.mli | 2 +-
plugins/fourier/Fourier.v | 2 +-
plugins/fourier/Fourier_util.v | 34 +-
plugins/fourier/fourier.ml | 2 +-
plugins/fourier/fourierR.ml | 2 +-
plugins/fourier/g_fourier.ml4 | 2 +-
plugins/funind/Recdef.v | 2 +-
plugins/funind/functional_principles_types.ml | 6 -
plugins/funind/g_indfun.ml4 | 2 +-
plugins/funind/invfun.ml | 2 +-
plugins/funind/merge.ml | 2 +-
plugins/funind/recdef.ml | 2 +-
plugins/micromega/CheckerMaker.v | 2 +-
plugins/micromega/Env.v | 153 +-
plugins/micromega/EnvRing.v | 1257 +++++--------
plugins/micromega/MExtraction.v | 4 +-
plugins/micromega/OrderedRing.v | 2 +-
plugins/micromega/Psatz.v | 8 +-
plugins/micromega/QMicromega.v | 10 +-
plugins/micromega/RMicromega.v | 30 +-
plugins/micromega/Refl.v | 2 +-
plugins/micromega/RingMicromega.v | 50 +-
plugins/micromega/Tauto.v | 2 +-
plugins/micromega/VarMap.v | 2 +-
plugins/micromega/ZCoeff.v | 16 +-
plugins/micromega/ZMicromega.v | 216 ++-
plugins/micromega/certificate.ml | 2 +-
plugins/micromega/coq_micromega.ml | 23 +-
plugins/micromega/csdpcert.ml | 2 +-
plugins/micromega/g_micromega.ml4 | 2 +-
plugins/micromega/mutils.ml | 2 +-
plugins/micromega/persistent_cache.ml | 32 +-
plugins/micromega/polynomial.ml | 2 +-
plugins/micromega/sos.mli | 2 +-
plugins/micromega/sos_types.ml | 2 +-
plugins/nsatz/Nsatz.v | 40 +-
plugins/nsatz/ideal.ml | 2 +-
plugins/nsatz/nsatz.ml4 | 2 +-
plugins/nsatz/polynom.ml | 2 +-
plugins/nsatz/polynom.mli | 2 +-
plugins/omega/Omega.v | 8 +-
plugins/omega/OmegaLemmas.v | 266 ++-
plugins/omega/OmegaPlugin.v | 2 +-
plugins/omega/PreOmega.v | 353 ++--
plugins/omega/coq_omega.ml | 59 +-
plugins/omega/g_omega.ml4 | 2 +-
plugins/omega/omega.ml | 2 +-
plugins/quote/Quote.v | 4 +-
plugins/quote/g_quote.ml4 | 2 +-
plugins/quote/quote.ml | 2 +-
plugins/ring/LegacyArithRing.v | 8 +-
plugins/ring/LegacyNArithRing.v | 25 +-
plugins/ring/LegacyRing.v | 6 +-
plugins/ring/LegacyRing_theory.v | 42 +-
plugins/ring/LegacyZArithRing.v | 8 +-
plugins/ring/Ring_abstract.v | 90 +-
plugins/ring/Ring_normalize.v | 142 +-
plugins/ring/Setoid_ring.v | 2 +-
plugins/ring/Setoid_ring_normalize.v | 122 +-
plugins/ring/Setoid_ring_theory.v | 4 +-
plugins/ring/g_ring.ml4 | 2 +-
plugins/ring/ring.ml | 8 +-
plugins/romega/ReflOmegaCore.v | 505 +++--
plugins/rtauto/Bintree.v | 16 +-
plugins/rtauto/Rtauto.v | 2 +-
plugins/rtauto/g_rtauto.ml4 | 2 +-
plugins/rtauto/proof_search.ml | 2 +-
plugins/rtauto/proof_search.mli | 2 +-
plugins/rtauto/refl_tauto.ml | 4 +-
plugins/rtauto/refl_tauto.mli | 2 +-
plugins/setoid_ring/ArithRing.v | 10 +-
plugins/setoid_ring/BinList.v | 77 +-
plugins/setoid_ring/Cring.v | 27 +-
plugins/setoid_ring/Field.v | 2 +-
plugins/setoid_ring/Field_tac.v | 6 +-
plugins/setoid_ring/Field_theory.v | 415 ++---
plugins/setoid_ring/InitialRing.v | 108 +-
plugins/setoid_ring/Integral_domain.v | 5 +-
plugins/setoid_ring/NArithRing.v | 2 +-
plugins/setoid_ring/Ncring.v | 35 +-
plugins/setoid_ring/Ncring_initial.v | 56 +-
plugins/setoid_ring/Ncring_polynom.v | 111 +-
plugins/setoid_ring/Ncring_tac.v | 10 +-
plugins/setoid_ring/RealField.v | 64 +-
plugins/setoid_ring/Ring.v | 4 +-
plugins/setoid_ring/Ring_base.v | 2 +-
plugins/setoid_ring/Ring_polynom.v | 1310 +++++--------
plugins/setoid_ring/Ring_tac.v | 7 +-
plugins/setoid_ring/Ring_theory.v | 293 ++-
plugins/setoid_ring/Rings_Z.v | 2 +-
plugins/setoid_ring/ZArithRing.v | 6 +-
plugins/setoid_ring/newring.ml4 | 2 +-
plugins/subtac/eterm.mli | 2 +-
plugins/subtac/g_subtac.ml4 | 2 +-
plugins/subtac/subtac.ml | 2 +-
plugins/subtac/subtac_cases.ml | 2 +-
plugins/subtac/subtac_cases.mli | 2 +-
plugins/subtac/subtac_classes.ml | 2 +-
plugins/subtac/subtac_classes.mli | 2 +-
plugins/subtac/subtac_coercion.ml | 2 +-
plugins/subtac/subtac_command.ml | 9 +-
plugins/subtac/subtac_pretyping.ml | 2 +-
plugins/subtac/subtac_pretyping_F.ml | 2 +-
plugins/syntax/nat_syntax.ml | 6 +-
plugins/syntax/numbers_syntax.ml | 96 +-
plugins/syntax/r_syntax.ml | 2 +-
plugins/syntax/z_syntax.ml | 2 +-
plugins/xml/dumptree.ml4 | 2 +-
pretyping/arguments_renaming.ml | 2 +-
pretyping/arguments_renaming.mli | 2 +-
pretyping/cases.ml | 2 +-
pretyping/cases.mli | 2 +-
pretyping/cbv.ml | 2 +-
pretyping/cbv.mli | 2 +-
pretyping/classops.ml | 2 +-
pretyping/classops.mli | 2 +-
pretyping/coercion.ml | 2 +-
pretyping/coercion.mli | 2 +-
pretyping/detyping.ml | 2 +-
pretyping/detyping.mli | 2 +-
pretyping/evarconv.ml | 36 +-
pretyping/evarconv.mli | 2 +-
pretyping/evarutil.ml | 85 +-
pretyping/evarutil.mli | 24 +-
pretyping/evd.ml | 2 +-
pretyping/evd.mli | 2 +-
pretyping/glob_term.ml | 2 +-
pretyping/glob_term.mli | 2 +-
pretyping/indrec.ml | 2 +-
pretyping/indrec.mli | 2 +-
pretyping/inductiveops.ml | 2 +-
pretyping/inductiveops.mli | 2 +-
pretyping/matching.ml | 2 +-
pretyping/matching.mli | 2 +-
pretyping/namegen.ml | 2 +-
pretyping/namegen.mli | 2 +-
pretyping/pattern.ml | 2 +-
pretyping/pattern.mli | 2 +-
pretyping/pretype_errors.ml | 2 +-
pretyping/pretype_errors.mli | 2 +-
pretyping/pretyping.ml | 16 +-
pretyping/pretyping.mli | 2 +-
pretyping/recordops.ml | 2 +-
pretyping/recordops.mli | 2 +-
pretyping/reductionops.ml | 2 +-
pretyping/reductionops.mli | 2 +-
pretyping/retyping.ml | 2 +-
pretyping/retyping.mli | 2 +-
pretyping/tacred.ml | 2 +-
pretyping/tacred.mli | 2 +-
pretyping/term_dnet.ml | 2 +-
pretyping/term_dnet.mli | 2 +-
pretyping/termops.ml | 2 +-
pretyping/termops.mli | 2 +-
pretyping/typeclasses.ml | 2 +-
pretyping/typeclasses.mli | 2 +-
pretyping/typeclasses_errors.ml | 2 +-
pretyping/typeclasses_errors.mli | 2 +-
pretyping/typing.ml | 2 +-
pretyping/typing.mli | 2 +-
pretyping/unification.ml | 26 +-
pretyping/unification.mli | 2 +-
pretyping/vnorm.ml | 2 +-
pretyping/vnorm.mli | 2 +-
proofs/clenv.ml | 2 +-
proofs/clenv.mli | 2 +-
proofs/clenvtac.ml | 6 +-
proofs/clenvtac.mli | 2 +-
proofs/evar_refiner.ml | 2 +-
proofs/evar_refiner.mli | 2 +-
proofs/goal.ml | 2 +-
proofs/goal.mli | 2 +-
proofs/logic.ml | 2 +-
proofs/logic.mli | 2 +-
proofs/pfedit.ml | 5 +-
proofs/pfedit.mli | 2 +-
proofs/proof.ml | 18 +-
proofs/proof.mli | 11 +-
proofs/proof_global.ml | 2 +-
proofs/proof_global.mli | 2 +-
proofs/proof_type.ml | 2 +-
proofs/proof_type.mli | 2 +-
proofs/proofview.ml | 7 +-
proofs/proofview.mli | 20 +-
proofs/redexpr.ml | 2 +-
proofs/redexpr.mli | 2 +-
proofs/refiner.ml | 2 +-
proofs/refiner.mli | 2 +-
proofs/tacexpr.ml | 14 +-
proofs/tacmach.ml | 2 +-
proofs/tacmach.mli | 2 +-
proofs/tactic_debug.ml | 2 +-
proofs/tactic_debug.mli | 2 +-
scripts/coqc.ml | 2 +-
scripts/coqmktop.ml | 41 +-
states/MakeInitial.v | 2 +-
tactics/auto.ml | 26 +-
tactics/auto.mli | 2 +-
tactics/autorewrite.ml | 2 +-
tactics/autorewrite.mli | 2 +-
tactics/btermdn.ml | 2 +-
tactics/btermdn.mli | 2 +-
tactics/class_tactics.ml4 | 2 +-
tactics/contradiction.ml | 2 +-
tactics/contradiction.mli | 2 +-
tactics/eauto.ml4 | 2 +-
tactics/eauto.mli | 2 +-
tactics/elim.ml | 2 +-
tactics/elim.mli | 2 +-
tactics/elimschemes.ml | 2 +-
tactics/elimschemes.mli | 2 +-
tactics/eqdecide.ml4 | 2 +-
tactics/eqschemes.ml | 2 +-
tactics/eqschemes.mli | 2 +-
tactics/equality.ml | 2 +-
tactics/equality.mli | 2 +-
tactics/evar_tactics.ml | 2 +-
tactics/evar_tactics.mli | 2 +-
tactics/extraargs.ml4 | 2 +-
tactics/extraargs.mli | 2 +-
tactics/extratactics.ml4 | 8 +-
tactics/extratactics.mli | 2 +-
tactics/hiddentac.ml | 25 +-
tactics/hiddentac.mli | 21 +-
tactics/hipattern.ml4 | 2 +-
tactics/hipattern.mli | 2 +-
tactics/inv.ml | 2 +-
tactics/inv.mli | 2 +-
tactics/leminv.ml | 2 +-
tactics/nbtermdn.ml | 2 +-
tactics/nbtermdn.mli | 2 +-
tactics/refine.ml | 2 +-
tactics/refine.mli | 2 +-
tactics/rewrite.ml4 | 247 ++-
tactics/tacinterp.ml | 65 +-
tactics/tacinterp.mli | 3 +-
tactics/tactic_option.ml | 2 +-
tactics/tactic_option.mli | 2 +-
tactics/tacticals.ml | 2 +-
tactics/tacticals.mli | 2 +-
tactics/tactics.ml | 21 +-
tactics/tactics.mli | 6 +-
tactics/tauto.ml4 | 2 +-
tactics/termdn.ml | 2 +-
tactics/termdn.mli | 2 +-
test-suite/bench/lists-100.v | 2 +-
test-suite/bench/lists_100.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1414.v | 4 +-
test-suite/bugs/closed/shouldsucceed/1784.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1844.v | 2 +-
test-suite/bugs/closed/shouldsucceed/1935.v | 2 +-
test-suite/bugs/closed/shouldsucceed/2127.v | 4 +-
test-suite/bugs/closed/shouldsucceed/2817.v | 9 +
test-suite/bugs/closed/shouldsucceed/2836.v | 39 +
test-suite/complexity/ring2.v | 7 +-
test-suite/failure/Tauto.v | 2 +-
test-suite/failure/Uminus.v | 4 +-
test-suite/failure/clash_cons.v | 2 +-
test-suite/failure/fixpoint1.v | 2 +-
test-suite/failure/guard.v | 2 +-
test-suite/failure/illtype1.v | 2 +-
test-suite/failure/pattern.v | 2 +-
test-suite/failure/positivity.v | 2 +-
test-suite/failure/redef.v | 2 +-
test-suite/failure/search.v | 2 +-
test-suite/failure/subtyping2.v | 20 +-
test-suite/failure/universes-buraliforti-redef.v | 20 +-
test-suite/failure/universes-buraliforti.v | 20 +-
test-suite/ideal-features/Apply.v | 2 +-
test-suite/ideal-features/eapply_evar.v | 2 +-
test-suite/micromega/example.v | 10 +-
test-suite/micromega/square.v | 18 +-
test-suite/misc/berardi_test.v | 14 +-
test-suite/modules/PO.v | 4 +-
test-suite/modules/Przyklad.v | 14 +-
test-suite/output/Notations.out | 5 +
test-suite/output/Notations.v | 9 +
test-suite/output/ZSyntax.out | 14 +-
test-suite/success/Check.v | 2 +-
test-suite/success/Field.v | 2 +-
test-suite/success/Funind.v | 22 +-
test-suite/success/Hints.v | 26 +-
test-suite/success/LegacyField.v | 2 +-
test-suite/success/MatchFail.v | 4 +-
test-suite/success/Mod_type.v | 12 +
test-suite/success/Notations.v | 5 +
test-suite/success/OmegaPre.v | 16 +-
test-suite/success/ProgramWf.v | 6 +-
test-suite/success/ROmegaPre.v | 16 +-
test-suite/success/RecTutorial.v | 10 +-
test-suite/success/Reg.v | 8 +-
test-suite/success/Scopes.v | 2 +-
test-suite/success/Tauto.v | 2 +-
test-suite/success/TestRefine.v | 2 +-
test-suite/success/Try.v | 2 +-
test-suite/success/apply.v | 6 +-
test-suite/success/change.v | 6 +-
test-suite/success/decl_mode.v | 10 +-
test-suite/success/dependentind.v | 2 +-
test-suite/success/eauto.v | 2 +-
test-suite/success/eqdecide.v | 2 +-
test-suite/success/extraction.v | 2 +-
test-suite/success/fix.v | 8 +-
test-suite/success/inds_type_sec.v | 2 +-
test-suite/success/induct.v | 2 +-
test-suite/success/ltac.v | 8 +-
test-suite/success/mutual_ind.v | 2 +-
test-suite/success/proof_using.v | 6 +
test-suite/success/remember.v | 2 +-
test-suite/success/searchabout.v | 2 +-
test-suite/success/setoid_test.v | 20 +-
test-suite/success/specialize.v | 28 +-
test-suite/success/unfold.v | 2 +-
test-suite/success/unicode_utf8.v | 2 +-
test-suite/success/univers.v | 4 +-
test-suite/typeclasses/NewSetoid.v | 2 +-
theories/Arith/Arith.v | 2 +-
theories/Arith/Arith_base.v | 2 +-
theories/Arith/Between.v | 8 +-
theories/Arith/Bool_nat.v | 4 +-
theories/Arith/Compare.v | 8 +-
theories/Arith/Compare_dec.v | 10 +-
theories/Arith/Div2.v | 18 +-
theories/Arith/EqNat.v | 18 +-
theories/Arith/Euclid.v | 20 +-
theories/Arith/Even.v | 6 +-
theories/Arith/Factorial.v | 8 +-
theories/Arith/Gt.v | 16 +-
theories/Arith/Le.v | 8 +-
theories/Arith/Lt.v | 12 +-
theories/Arith/Max.v | 2 +-
theories/Arith/Min.v | 4 +-
theories/Arith/Minus.v | 32 +-
theories/Arith/Mult.v | 24 +-
theories/Arith/Peano_dec.v | 6 +-
theories/Arith/Plus.v | 32 +-
theories/Arith/Wf_nat.v | 22 +-
theories/Bool/Bool.v | 8 +-
theories/Bool/BoolEq.v | 6 +-
theories/Bool/Bvector.v | 4 +-
theories/Bool/DecBool.v | 2 +-
theories/Bool/IfProp.v | 2 +-
theories/Bool/Sumbool.v | 2 +-
theories/Bool/Zerob.v | 4 +-
theories/Classes/EquivDec.v | 4 +-
theories/Classes/Equivalence.v | 6 +-
theories/Classes/Init.v | 2 +-
theories/Classes/Morphisms.v | 4 +-
theories/Classes/Morphisms_Prop.v | 2 +-
theories/Classes/Morphisms_Relations.v | 2 +-
theories/Classes/RelationClasses.v | 4 +-
theories/Classes/SetoidClass.v | 2 +-
theories/Classes/SetoidDec.v | 4 +-
theories/Classes/SetoidTactics.v | 4 +-
theories/FSets/FMapAVL.v | 20 +-
theories/FSets/FMapFullAVL.v | 4 +-
theories/FSets/FMapPositive.v | 2 +-
theories/FSets/FSetBridge.v | 148 +-
theories/FSets/FSetEqProperties.v | 8 +-
theories/FSets/FSetFacts.v | 6 +-
theories/FSets/FSetProperties.v | 2 +-
theories/Init/Datatypes.v | 24 +-
theories/Init/Logic.v | 24 +-
theories/Init/Logic_Type.v | 12 +-
theories/Init/Notations.v | 2 +-
theories/Init/Peano.v | 26 +-
theories/Init/Prelude.v | 2 +-
theories/Init/Specif.v | 28 +-
theories/Init/Tactics.v | 12 +-
theories/Init/Wf.v | 4 +-
theories/Lists/List.v | 48 +-
theories/Lists/ListSet.v | 78 +-
theories/Lists/ListTactics.v | 4 +-
theories/Lists/SetoidList.v | 90 +-
theories/Lists/SetoidPermutation.v | 125 ++
theories/Lists/StreamMemo.v | 29 +-
theories/Lists/Streams.v | 14 +-
theories/Lists/vo.itarget | 1 +
theories/Logic/Berardi.v | 14 +-
theories/Logic/ChoiceFacts.v | 6 +-
theories/Logic/Classical.v | 2 +-
theories/Logic/ClassicalChoice.v | 2 +-
theories/Logic/ClassicalDescription.v | 4 +-
theories/Logic/ClassicalEpsilon.v | 2 +-
theories/Logic/ClassicalFacts.v | 38 +-
theories/Logic/ClassicalUniqueChoice.v | 2 +-
theories/Logic/Classical_Pred_Set.v | 2 +-
theories/Logic/Classical_Pred_Type.v | 10 +-
theories/Logic/Classical_Prop.v | 10 +-
theories/Logic/Classical_Type.v | 2 +-
theories/Logic/ConstructiveEpsilon.v | 6 +-
theories/Logic/Decidable.v | 2 +-
theories/Logic/Description.v | 2 +-
theories/Logic/Diaconescu.v | 16 +-
theories/Logic/Epsilon.v | 2 +-
theories/Logic/Eqdep.v | 2 +-
theories/Logic/EqdepFacts.v | 14 +-
theories/Logic/Eqdep_dec.v | 32 +-
theories/Logic/ExtensionalityFacts.v | 2 +-
theories/Logic/FunctionalExtensionality.v | 2 +-
theories/Logic/Hurkens.v | 6 +-
theories/Logic/IndefiniteDescription.v | 2 +-
theories/Logic/JMeq.v | 2 +-
theories/Logic/ProofIrrelevance.v | 2 +-
theories/Logic/ProofIrrelevanceFacts.v | 4 +-
theories/Logic/RelationalChoice.v | 2 +-
theories/Logic/SetIsType.v | 2 +-
theories/MSets/MSetEqProperties.v | 8 +-
theories/MSets/MSetInterface.v | 2 +-
theories/MSets/MSetList.v | 6 +-
theories/MSets/MSetPositive.v | 4 +-
theories/MSets/MSetProperties.v | 2 +-
theories/MSets/MSetRBT.v | 104 +-
theories/MSets/MSetWeakList.v | 6 +-
theories/NArith/BinNat.v | 220 +--
theories/NArith/BinNatDef.v | 94 +-
theories/NArith/NArith.v | 2 +-
theories/NArith/Ndec.v | 443 ++---
theories/NArith/Ndigits.v | 207 +--
theories/NArith/Ndist.v | 104 +-
theories/NArith/Ndiv_def.v | 14 +-
theories/NArith/Ngcd_def.v | 2 +-
theories/NArith/Nnat.v | 56 +-
theories/NArith/Nsqrt_def.v | 12 +-
theories/Numbers/BigNumPrelude.v | 163 +-
theories/Numbers/BinNums.v | 2 +-
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 46 +-
theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 50 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 115 +-
.../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 30 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 272 +--
theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 80 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 186 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 88 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 393 ++--
theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 26 +-
theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 4 +-
theories/Numbers/Cyclic/Int31/Cyclic31.v | 609 +++---
theories/Numbers/Cyclic/Int31/Int31.v | 18 +-
theories/Numbers/Cyclic/Int31/Ring31.v | 4 +-
theories/Numbers/Cyclic/ZModulo/ZModulo.v | 191 +-
theories/Numbers/Integer/Abstract/ZAdd.v | 2 +-
theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +-
theories/Numbers/Integer/Abstract/ZBase.v | 2 +-
theories/Numbers/Integer/Abstract/ZBits.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +-
theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 +-
theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
theories/Numbers/Integer/Abstract/ZGcd.v | 2 +-
theories/Numbers/Integer/Abstract/ZLcm.v | 2 +-
theories/Numbers/Integer/Abstract/ZLt.v | 2 +-
theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +-
theories/Numbers/Integer/Abstract/ZMul.v | 2 +-
theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +-
theories/Numbers/Integer/Abstract/ZParity.v | 2 +-
theories/Numbers/Integer/Abstract/ZPow.v | 13 +-
theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +-
theories/Numbers/Integer/BigZ/BigZ.v | 10 +-
theories/Numbers/Integer/BigZ/ZMake.v | 454 ++---
theories/Numbers/Integer/Binary/ZBinary.v | 4 +-
theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 +-
theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +-
theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 6 +-
theories/Numbers/NaryFunctions.v | 2 +-
theories/Numbers/NatInt/NZAdd.v | 2 +-
theories/Numbers/NatInt/NZAddOrder.v | 2 +-
theories/Numbers/NatInt/NZAxioms.v | 4 +-
theories/Numbers/NatInt/NZBase.v | 2 +-
theories/Numbers/NatInt/NZBits.v | 2 +-
theories/Numbers/NatInt/NZDiv.v | 2 +-
theories/Numbers/NatInt/NZDomain.v | 2 +-
theories/Numbers/NatInt/NZGcd.v | 2 +-
theories/Numbers/NatInt/NZLog.v | 2 +-
theories/Numbers/NatInt/NZMul.v | 2 +-
theories/Numbers/NatInt/NZMulOrder.v | 6 +-
theories/Numbers/NatInt/NZOrder.v | 2 +-
theories/Numbers/NatInt/NZParity.v | 2 +-
theories/Numbers/NatInt/NZPow.v | 2 +-
theories/Numbers/NatInt/NZProperties.v | 2 +-
theories/Numbers/NatInt/NZSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NAdd.v | 2 +-
theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NAxioms.v | 2 +-
theories/Numbers/Natural/Abstract/NBase.v | 2 +-
theories/Numbers/Natural/Abstract/NBits.v | 4 +-
theories/Numbers/Natural/Abstract/NDefOps.v | 4 +-
theories/Numbers/Natural/Abstract/NDiv.v | 2 +-
theories/Numbers/Natural/Abstract/NGcd.v | 2 +-
theories/Numbers/Natural/Abstract/NIso.v | 2 +-
theories/Numbers/Natural/Abstract/NLcm.v | 2 +-
theories/Numbers/Natural/Abstract/NLog.v | 2 +-
theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +-
theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NOrder.v | 2 +-
theories/Numbers/Natural/Abstract/NParity.v | 2 +-
theories/Numbers/Natural/Abstract/NPow.v | 2 +-
theories/Numbers/Natural/Abstract/NProperties.v | 2 +-
theories/Numbers/Natural/Abstract/NSqrt.v | 2 +-
theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +-
theories/Numbers/Natural/Abstract/NSub.v | 2 +-
theories/Numbers/Natural/BigN/BigN.v | 4 +-
theories/Numbers/Natural/BigN/NMake.v | 364 ++--
theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
theories/Numbers/Natural/BigN/Nbasic.v | 120 +-
theories/Numbers/Natural/Binary/NBinary.v | 6 +-
theories/Numbers/Natural/Peano/NPeano.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSig.v | 2 +-
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 10 +-
theories/Numbers/NumPrelude.v | 2 +-
theories/Numbers/Rational/BigQ/BigQ.v | 10 +-
theories/Numbers/Rational/BigQ/QMake.v | 485 +++--
theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +-
theories/PArith/BinPos.v | 364 ++--
theories/PArith/BinPosDef.v | 5 +-
theories/PArith/PArith.v | 2 +-
theories/PArith/POrderedType.v | 2 +-
theories/PArith/Pnat.v | 81 +-
theories/Program/Basics.v | 4 +-
theories/Program/Combinators.v | 2 +-
theories/Program/Equality.v | 12 +-
theories/Program/Program.v | 2 +-
theories/Program/Subset.v | 6 +-
theories/Program/Syntax.v | 2 +-
theories/Program/Tactics.v | 4 +-
theories/Program/Utils.v | 2 +-
theories/Program/Wf.v | 6 +-
theories/QArith/QArith.v | 2 +-
theories/QArith/QArith_base.v | 255 ++-
theories/QArith/QOrderedType.v | 2 +-
theories/QArith/Qabs.v | 26 +-
theories/QArith/Qcanon.v | 22 +-
theories/QArith/Qfield.v | 6 +-
theories/QArith/Qminmax.v | 2 +-
theories/QArith/Qpower.v | 88 +-
theories/QArith/Qreals.v | 62 +-
theories/QArith/Qreduction.v | 166 +-
theories/QArith/Qring.v | 2 +-
theories/QArith/Qround.v | 26 +-
theories/Reals/Alembert.v | 254 +--
theories/Reals/AltSeries.v | 122 +-
theories/Reals/ArithProp.v | 50 +-
theories/Reals/Binomial.v | 68 +-
theories/Reals/Cauchy_prod.v | 28 +-
theories/Reals/Cos_plus.v | 194 +-
theories/Reals/Cos_rel.v | 92 +-
theories/Reals/DiscrR.v | 10 +-
theories/Reals/Exp_prop.v | 230 ++-
theories/Reals/Integration.v | 2 +-
theories/Reals/LegacyRfield.v | 6 +-
theories/Reals/MVT.v | 102 +-
theories/Reals/Machin.v | 168 ++
theories/Reals/NewtonInt.v | 158 +-
theories/Reals/PSeries_reg.v | 62 +-
theories/Reals/PartSum.v | 142 +-
theories/Reals/RIneq.v | 266 +--
theories/Reals/RList.v | 232 +--
theories/Reals/ROrderedType.v | 2 +-
theories/Reals/R_Ifp.v | 80 +-
theories/Reals/R_sqr.v | 36 +-
theories/Reals/R_sqrt.v | 56 +-
theories/Reals/Ranalysis.v | 775 +-------
theories/Reals/Ranalysis1.v | 362 ++--
theories/Reals/Ranalysis2.v | 92 +-
theories/Reals/Ranalysis3.v | 162 +-
theories/Reals/Ranalysis4.v | 106 +-
theories/Reals/Ranalysis5.v | 1348 ++++++++++++++
theories/Reals/Ranalysis_reg.v | 800 ++++++++
theories/Reals/Ratan.v | 1602 ++++++++++++++++
theories/Reals/Raxioms.v | 8 +-
theories/Reals/Rbase.v | 2 +-
theories/Reals/Rbasic_fun.v | 102 +-
theories/Reals/Rcomplete.v | 50 +-
theories/Reals/Rdefinitions.v | 4 +-
theories/Reals/Rderiv.v | 114 +-
theories/Reals/Reals.v | 2 +-
theories/Reals/Rfunctions.v | 119 +-
theories/Reals/Rgeom.v | 32 +-
theories/Reals/RiemannInt.v | 898 ++++-----
theories/Reals/RiemannInt_SF.v | 954 +++++-----
theories/Reals/Rlimit.v | 106 +-
theories/Reals/Rlogic.v | 10 +-
theories/Reals/Rminmax.v | 2 +-
theories/Reals/Rpow_def.v | 2 +-
theories/Reals/Rpower.v | 168 +-
theories/Reals/Rprod.v | 20 +-
theories/Reals/Rseries.v | 44 +-
theories/Reals/Rsigma.v | 34 +-
theories/Reals/Rsqrt_def.v | 216 +--
theories/Reals/Rtopology.v | 694 +++----
theories/Reals/Rtrigo.v | 1796 +-----------------
theories/Reals/Rtrigo1.v | 1933 ++++++++++++++++++++
theories/Reals/Rtrigo_alt.v | 163 +-
theories/Reals/Rtrigo_calc.v | 112 +-
theories/Reals/Rtrigo_def.v | 108 +-
theories/Reals/Rtrigo_fun.v | 30 +-
theories/Reals/Rtrigo_reg.v | 308 +---
theories/Reals/SeqProp.v | 270 +--
theories/Reals/SeqSeries.v | 98 +-
theories/Reals/SplitAbsolu.v | 4 +-
theories/Reals/SplitRmult.v | 2 +-
theories/Reals/Sqrt_reg.v | 150 +-
theories/Reals/vo.itarget | 5 +
theories/Relations/Operators_Properties.v | 8 +-
theories/Relations/Relation_Definitions.v | 2 +-
theories/Relations/Relation_Operators.v | 8 +-
theories/Relations/Relations.v | 8 +-
theories/Setoids/Setoid.v | 2 +-
theories/Sets/Classical_sets.v | 18 +-
theories/Sets/Constructive_sets.v | 18 +-
theories/Sets/Cpo.v | 2 +-
theories/Sets/Ensembles.v | 2 +-
theories/Sets/Finite_sets.v | 6 +-
theories/Sets/Finite_sets_facts.v | 20 +-
theories/Sets/Image.v | 12 +-
theories/Sets/Infinite_sets.v | 14 +-
theories/Sets/Integers.v | 24 +-
theories/Sets/Multiset.v | 18 +-
theories/Sets/Partial_Order.v | 20 +-
theories/Sets/Permut.v | 2 +-
theories/Sets/Powerset.v | 28 +-
theories/Sets/Powerset_Classical_facts.v | 42 +-
theories/Sets/Powerset_facts.v | 36 +-
theories/Sets/Relations_1.v | 2 +-
theories/Sets/Relations_1_facts.v | 20 +-
theories/Sets/Relations_2.v | 2 +-
theories/Sets/Relations_2_facts.v | 14 +-
theories/Sets/Relations_3.v | 2 +-
theories/Sets/Relations_3_facts.v | 28 +-
theories/Sets/Uniset.v | 30 +-
theories/Sorting/Heap.v | 22 +-
theories/Sorting/Mergesort.v | 4 +-
theories/Sorting/PermutEq.v | 2 +-
theories/Sorting/PermutSetoid.v | 12 +-
theories/Sorting/Permutation.v | 2 +-
theories/Sorting/Sorted.v | 2 +-
theories/Sorting/Sorting.v | 2 +-
theories/Strings/Ascii.v | 16 +-
theories/Strings/String.v | 130 +-
theories/Structures/DecidableTypeEx.v | 6 +-
theories/Structures/OrderedTypeEx.v | 160 +-
theories/Structures/OrdersAlt.v | 6 +-
theories/Unicode/Utf8.v | 4 +-
theories/Unicode/Utf8_core.v | 2 +-
theories/Vectors/VectorDef.v | 2 +-
theories/Wellfounded/Disjoint_Union.v | 4 +-
theories/Wellfounded/Inclusion.v | 4 +-
theories/Wellfounded/Inverse_Image.v | 6 +-
.../Wellfounded/Lexicographic_Exponentiation.v | 28 +-
theories/Wellfounded/Lexicographic_Product.v | 10 +-
theories/Wellfounded/Transitive_Closure.v | 6 +-
theories/Wellfounded/Union.v | 6 +-
theories/Wellfounded/Well_Ordering.v | 8 +-
theories/Wellfounded/Wellfounded.v | 2 +-
theories/ZArith/BinInt.v | 804 ++++----
theories/ZArith/BinIntDef.v | 253 +--
theories/ZArith/Int.v | 16 +-
theories/ZArith/Wf_Z.v | 12 +-
theories/ZArith/ZArith.v | 2 +-
theories/ZArith/ZArith_base.v | 2 +-
theories/ZArith/ZArith_dec.v | 93 +-
theories/ZArith/Zabs.v | 56 +-
theories/ZArith/Zbool.v | 16 +-
theories/ZArith/Zcompare.v | 34 +-
theories/ZArith/Zcomplements.v | 14 +-
theories/ZArith/Zdigits.v | 58 +-
theories/ZArith/Zdiv.v | 86 +-
theories/ZArith/Zeuclid.v | 2 +-
theories/ZArith/Zeven.v | 22 +-
theories/ZArith/Zgcd_alt.v | 241 ++-
theories/ZArith/Zhints.v | 95 +-
theories/ZArith/Zlogarithm.v | 104 +-
theories/ZArith/Zmax.v | 121 +-
theories/ZArith/Zmin.v | 92 +-
theories/ZArith/Zminmax.v | 16 +-
theories/ZArith/Zmisc.v | 11 +-
theories/ZArith/Znat.v | 162 +-
theories/ZArith/Znumtheory.v | 385 ++--
theories/ZArith/Zorder.v | 100 +-
theories/ZArith/Zpow_alt.v | 4 +-
theories/ZArith/Zpow_def.v | 14 +-
theories/ZArith/Zpow_facts.v | 42 +-
theories/ZArith/Zpower.v | 14 +-
theories/ZArith/Zquot.v | 351 ++--
theories/ZArith/Zsqrt_compat.v | 63 +-
theories/ZArith/Zwf.v | 27 +-
theories/ZArith/auxiliary.v | 2 +-
tools/compat5.ml | 2 +-
tools/compat5.mlp | 2 +-
tools/compat5b.ml | 2 +-
tools/compat5b.mlp | 2 +-
tools/coq_makefile.ml | 6 +-
tools/coq_tex.ml4 | 2 +-
tools/coqdep.ml | 2 +-
tools/coqdep_boot.ml | 2 +-
tools/coqdep_common.ml | 2 +-
tools/coqdep_common.mli | 2 +-
tools/coqdep_lexer.mli | 2 +-
tools/coqdep_lexer.mll | 2 +-
tools/coqdoc/alpha.ml | 2 +-
tools/coqdoc/alpha.mli | 2 +-
tools/coqdoc/cdglobals.ml | 2 +-
tools/coqdoc/cpretty.mli | 2 +-
tools/coqdoc/cpretty.mll | 71 +-
tools/coqdoc/index.ml | 13 +-
tools/coqdoc/index.mli | 2 +-
tools/coqdoc/main.ml | 2 +-
tools/coqdoc/output.ml | 151 +-
tools/coqdoc/output.mli | 13 +-
tools/coqdoc/tokens.ml | 2 +-
tools/coqdoc/tokens.mli | 2 +-
tools/coqwc.mll | 2 +-
tools/escape_string.ml | 1 +
tools/fake_ide.ml | 2 +-
tools/gallina.ml | 2 +-
tools/gallina_lexer.mll | 2 +-
tools/mingwpath.ml | 15 +
toplevel/auto_ind_decl.ml | 2 +-
toplevel/auto_ind_decl.mli | 2 +-
toplevel/autoinstance.ml | 2 +-
toplevel/autoinstance.mli | 2 +-
toplevel/backtrack.ml | 22 +-
toplevel/backtrack.mli | 10 +-
toplevel/cerrors.ml | 2 +-
toplevel/cerrors.mli | 2 +-
toplevel/class.ml | 2 +-
toplevel/class.mli | 2 +-
toplevel/classes.ml | 2 +-
toplevel/classes.mli | 2 +-
toplevel/command.ml | 9 +-
toplevel/command.mli | 2 +-
toplevel/coqinit.ml | 10 +-
toplevel/coqinit.mli | 4 +-
toplevel/coqtop.ml | 21 +-
toplevel/coqtop.mli | 2 +-
toplevel/discharge.ml | 2 +-
toplevel/discharge.mli | 2 +-
toplevel/himsg.ml | 57 +-
toplevel/himsg.mli | 2 +-
toplevel/ide_intf.ml | 43 +-
toplevel/ide_intf.mli | 2 +-
toplevel/ide_slave.ml | 45 +-
toplevel/ide_slave.mli | 2 +-
toplevel/ind_tables.ml | 2 +-
toplevel/ind_tables.mli | 2 +-
toplevel/indschemes.ml | 2 +-
toplevel/indschemes.mli | 2 +-
toplevel/interface.mli | 16 +-
toplevel/lemmas.ml | 2 +-
toplevel/lemmas.mli | 2 +-
toplevel/libtypes.ml | 2 +-
toplevel/libtypes.mli | 2 +-
toplevel/metasyntax.ml | 20 +-
toplevel/metasyntax.mli | 4 +-
toplevel/mltop.ml4 | 135 +-
toplevel/mltop.mli | 25 +-
toplevel/record.ml | 2 +-
toplevel/record.mli | 2 +-
toplevel/search.ml | 2 +-
toplevel/search.mli | 2 +-
toplevel/toplevel.ml | 2 +-
toplevel/toplevel.mli | 2 +-
toplevel/usage.ml | 4 +-
toplevel/usage.mli | 2 +-
toplevel/vernac.ml | 39 +-
toplevel/vernac.mli | 2 +-
toplevel/vernacentries.ml | 141 +-
toplevel/vernacentries.mli | 4 +-
toplevel/vernacexpr.ml | 18 +-
toplevel/vernacinterp.ml | 2 +-
toplevel/vernacinterp.mli | 2 +-
toplevel/whelp.ml4 | 2 +-
toplevel/whelp.mli | 2 +-
1107 files changed, 21802 insertions(+), 18994 deletions(-)
delete mode 100644 INSTALL.macosx
create mode 100644 TODO
delete mode 100644 config/Makefile.template
create mode 100755 dev/macosify_accel.sh
delete mode 100644 doc/refman/RefMan-sch.tex
create mode 100644 test-suite/bugs/closed/shouldsucceed/2817.v
create mode 100644 test-suite/bugs/closed/shouldsucceed/2836.v
create mode 100644 theories/Lists/SetoidPermutation.v
create mode 100644 theories/Reals/Machin.v
create mode 100644 theories/Reals/Ranalysis5.v
create mode 100644 theories/Reals/Ranalysis_reg.v
create mode 100644 theories/Reals/Ratan.v
create mode 100644 theories/Reals/Rtrigo1.v
create mode 100644 tools/escape_string.ml
create mode 100644 tools/mingwpath.ml
(limited to 'theories/MSets/MSetRBT.v')
diff --git a/.gitignore b/.gitignore
index 32a40af6..e0be678c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,11 +63,12 @@ doc/refman/csdp.cache
doc/refman/trace
doc/refman/Reference-Manual.pdf
doc/refman/Reference-Manual.ps
+doc/refman/Reference-Manual.html
+doc/refman/Reference-Manual.out
+doc/refman/Reference-Manual.sh
doc/refman/cover.html
doc/refman/styles.hva
-doc/refman/Reference-Manual.html
doc/common/version.tex
-doc/refman/Reference-Manual.sh
doc/refman/coqide-queries.eps
doc/refman/coqide.eps
doc/refman/euclid.ml
diff --git a/CHANGES b/CHANGES
index c245fb25..1c094584 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,29 +1,66 @@
-Changes from V8.4beta to V8.4
-=============================
+Changes from V8.4beta2 to V8.4
+==============================
+
+Vernacular commands
+
+- The "Reset" command is now supported again in files given to coqc or Load.
+- "Show Script" now indents again the displayed scripts. It can also work
+ correctly across Load'ed files if the option "Unset Atomic Load" is used.
+- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
+ scope name (e.g. Z_scope).
+
+Notations
+
+- Most compatibility notations of the standard library are now tagged as
+ (compat xyz), where xyz is a former Coq version, for instance "8.3".
+ These notations behave as (only parsing) notations, except that they may
+ triggers warnings (or errors) when used while Coq is not in a corresponding
+ -compat mode.
+- To activate these compatibility warnings, use "Set Verbose Compat Notations"
+ or the command-line flag -verbose-compat-notations.
+- For a strict mode without these compatibility notations, use
+ "Unset Compat Notations" or the command-line flag -no-compat-notations.
+
+Tactics
+
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+ or "induction" to make it generate equations in the spirit of "case_eq".
+ The former syntax "_eqn" is discontinued.
+- The name of the hypothesis introduced by tactic "remember" can be
+ set via the new syntax "remember t as x eqn:H" (wish #2489).
+
+Libraries
+
+- Reals: changed definition of PI, no more axiom about sin(PI/2).
+- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
+- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
+
+Changes from V8.4beta to V8.4beta2
+==================================
Vernacular commands
-- Undo and UndoTo are now handling the proof states. They may
- perform some extra steps of backtrack to avoid states where
- the proof state is unavailable (typically a closed proof).
-- The commands Suspend and Resume have been removed.
+- Commands "Back" and "BackTo" are now handling the proof states. They may
+ perform some extra steps of backtrack to avoid states where the proof
+ state is unavailable (typically a closed proof).
+- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
-- New command "Grab Existential Variables" to transform the unresolved evars at
- the end of a proof into goals.
+- New command "Grab Existential Variables" to transform the unresolved evars
+ at the end of a proof into goals.
Tactics
-- Still no general "info" tactical, but new specific tactics
- info_auto, info_eauto, info_trivial which provides information
- on the proofs found by auto/eauto/trivial. Display of these
- details could also be activated by Set Info Auto/Eauto/Trivial.
-- Details on everything tried by auto/eauto/trivial during
- a proof search could be obtained by "debug auto", "debug eauto",
- "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
-- New command "r string" that interprets "idtac string" as a breakpoint
- and jumps to its next use in Ltac debugger.
+- Still no general "info" tactical, but new specific tactics info_auto,
+ info_eauto, info_trivial which provides information on the proofs found
+ by auto/eauto/trivial. Display of these details could also be activated by
+ "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
+- Details on everything tried by auto/eauto/trivial during a proof search
+ could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
+ global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
+- New command "r string" in Ltac debugger that interprets "idtac
+ string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
@@ -31,28 +68,28 @@ Tactics
Libraries
-- MSetRBT : a new implementation of MSets via Red-Black trees (initial
+- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
-- MSetAVL : for maximal sharing with the new MSetRBT, the argument order
- of Node has changed (this should be transparent to regular MSets users).
+- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
+ of Node has changed (this should be transparent to regular MSets users).
Module System
- The names of modules (and module types) are now in a fully separated
- namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+ namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
CoqIDE
-- Coqide now supports the Restart command, and Undo (with a warning).
- Better support for Abort.
+- Coqide now supports the "Restart" command, and "Undo" (with a warning).
+ Better support for "Abort".
Changes from V8.3 to V8.4beta
=============================
Logic
-- Standard eta-conversion now supported (dependent product only). (DOC TO DO)
+- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
@@ -69,10 +106,6 @@ Specification language and notations
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
-- In a pattern containing a "match", a final "| _ => _" branch could be used
- now instead of enumerating all remaining constructors. Moreover, the pattern
- "match _ with _ => _ end" now allows to match any "match". A "in" annotation
- can also be added to restrict to a precise inductive type.
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
@@ -81,11 +114,11 @@ Tactics
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
- delimitation via { }. Note: for use with ProofGeneral, a cvs version of
- ProofGeneral no older than mid-July 2011 is currently required. DOC TODO.
+ delimitation via { }. Note: for use with Proof General, a cvs version of
+ Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
-- New tactics constr_eq, is_evar and has_evar.
+- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout ". Since is a time
in second for the moment, this feature should rather be avoided
@@ -98,14 +131,14 @@ Tactics
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
- existential variables (theoretical source of possible incompatibility).
+ existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
- use the goal to complete the pattern assuming it is no ambiguous.
+ use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
@@ -118,18 +151,25 @@ Tactics
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
-- The behavior of the simpl tactic can be tuned using the new "Arguments"
- vernacular.
+- In an ltac pattern containing a "match", a final "| _ => _" branch could be
+ used now instead of enumerating all remaining constructors. Moreover, the
+ pattern "match _ with _ => _ end" now allows to match any "match". A "in"
+ annotation can also be added to restrict to a precise inductive type.
+- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
+ In particular constants can be marked so that they are always/never unfolded
+ by "simpl", or unfolded only when a set of arguments evaluates to a
+ constructor. Last one can mark a constant so that it is unfolded only if the
+ simplified term does not expose a match in head position.
Vernacular commands
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
-- New command "Add/Remove Search Blacklist ..." :
+- New command "Add/Remove Search Blacklist ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
- The default blacklisted substrings are "_admitted" "_subproof" "Private_". DOC TODO
+ The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
@@ -141,7 +181,11 @@ Vernacular commands
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
-- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope".
+- Command "Proof" accept a new modifier "using" to force generalization
+ over a given list of section variables at section ending.
+- New command "Arguments" generalizing "Implicit Arguments" and
+ "Arguments Scope" and that also allows to rename the parameters of a
+ definition and to tune the behavior of the tactic "simpl".
Module System
@@ -155,8 +199,8 @@ Module System
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
- the flag "Set Inline Level ..." to set a level. TODO: DOC!
-- Print Assumptions should now handle correctly opaque modules (#2168)
+ the flag "Set Inline Level ..." to set a level.
+- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
@@ -166,9 +210,9 @@ Module System
Libraries
- Extension of the abstract part of Numbers, which now provide axiomatizations
- and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2
- and bitwise functions. These functions are implemented for nat N BigN Z BigZ.
- See in particular file NPeano for new functions about nat.
+ and results about many more integer functions, such as pow, gcd, lcm, sqrt,
+ log2 and bitwise functions. These functions are implemented for nat, N, BigN,
+ Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
@@ -207,15 +251,15 @@ Libraries
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
-- Creation of Vector, an independant library for list indiced by their length.
- Vectors' names overwrite lists' one so you shouldn't "Import" the library.
- All old names change: functions' name become the CaML one and for example
- Vcons become Vector.cons. You can use notations by importing
+- Creation of Vector, an independent library for lists indexed by their length.
+ Vectors' names overwrite lists' one so you should not "Import" the library.
+ All old names changed: function names follow the ocaml ones and, for example,
+ Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
-- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
+- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
-- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument)
+- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Internal infrastructure
@@ -230,8 +274,8 @@ Internal infrastructure
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
-- new Makefile rules mli-doc to make html of mli in dev/doc/html and
- full-stdlib to get a HUGE pdf with all the stdlib.
+- New Makefile rules mli-doc to make html of mli in dev/doc/html and
+ full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
@@ -243,9 +287,8 @@ Extraction
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- DOC TODO.
- New option "Set/Unset Extraction KeepSingleton" for preventing the
- extraction to optimize singleton container types. DOC TODO
+ extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
@@ -257,10 +300,9 @@ CoqIDE
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
-- The communication between CoqIDE and Coqtop is now done via a dialect
- of XML (DOC TODO).
-- The backtrack engine of CoqIDE has been reworked, it now used the
- "Backtrack" command similarly to ProofGeneral.
+- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
+- The backtrack engine of CoqIDE has been reworked, it now uses the
+ "Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
@@ -274,15 +316,15 @@ Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
-- coq_makefile major cleanup.
- * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work
+- Major changes to coq_makefile:
+ * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
- with the same policy as vo in COQLIB
+ with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
- should work directly on any architecture.
+ should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
- be made in $XDG_DATA_HOME/coq.
+ be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
Changes from V8.2 to V8.3
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 0849b64f..41474202 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -3,4 +3,49 @@ Potential sources of incompatibilities between Coq V8.3 and V8.4
(see also file CHANGES)
-TO BE DONE
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+ Several definitions have new names or are defined in modules of
+ different names, but a special care has been taken to have this
+ renaming transparent for the user thanks to compatibility notations.
+
+ However some definitions have changed, what might require some
+ adaptations. The most noticeable examples are:
+ - The "?=" notation which now bind to Pos.compare rather than former
+ Pcompare (now Pos.compare_cont).
+ - Changes in names may induce different automatically generated
+ names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+ - Z.add has a new definition, hence, applying "simpl" on subterms of
+ its body might give different results than before.
+ - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+ power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+ - The definition of functions over "vectors" (list of fixed length)
+ have changed.
+ - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+ - Less unfolding of fixpoints when applying destruct or inversion on
+ a fixpoint hiding an inductive type (add an extra call to simpl to
+ preserve compatibility).
+ - Less unexpected local definitions when applying "destruct"
+ (incompatibilities solvable by adapting name hypotheses).
+ - Tactic "apply" might succeed more often, e.g. by now solving
+ pattern-matching of the form ?f x y = g(x,y) (compatibility
+ ensured by using "Unset Tactic Pattern Unification"), but also
+ because it supports (full) betaiota (using "simple apply" might
+ then help).
+ - Tactic autorewrite does no longer instantiate pre-existing
+ existential variables.
+ - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+ - The command "Load" is now atomic for backtracking (use "Unset
+ Atomic Load" for compatibility).
diff --git a/INSTALL b/INSTALL
index 5ee00613..02c9eb9b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,5 +1,5 @@
- INSTALLATION PROCEDURES FOR THE COQ V8.3 SYSTEM
+ INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM
-----------------------------------------------
diff --git a/INSTALL.macosx b/INSTALL.macosx
deleted file mode 100644
index cc1317b1..00000000
--- a/INSTALL.macosx
+++ /dev/null
@@ -1,20 +0,0 @@
-INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X
-------------------------------------------------------------------------
-
-You can also use fink, or the MacOS X package prepared by the Coq
-team. To use the MacOS X package,:
-
-1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer)
- or coq-8.1-macosx-i386.dmg (for Pentium-based computer).
-
-2) Double-click on its icon; it mounts a disk volume named "Coq V8.1".
-
-3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the
- installer (you'll need administrator permissions).
-
-4) Coq installs in /usr/local/bin, which should be in your PATH, and
- can be used from a Terminal window: the interactive toplevel is
- named coqtop and the compiler is coqc.
-
-If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
diff --git a/Makefile b/Makefile
index 0ff72856..bb5ec3bc 100644
--- a/Makefile
+++ b/Makefile
@@ -39,9 +39,13 @@
# File lists
###########################################################################
+# NB: due to limitations in Win32, please refrain using 'export' too much
+# to communicate between make sub-calls (in Win32, 8kb max per env variable,
+# 32kb total)
+
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
-export FIND_VCS_CLAUSE:='(' \
+FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
-name '_darcs' -o \
@@ -58,8 +62,8 @@ endef
## Files in the source tree
-export YACCFILES:=$(call find, '*.mly')
-export LEXFILES := $(call find, '*.mll')
+YACCFILES:=$(call find, '*.mly')
+LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')
@@ -73,13 +77,13 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+GENML4FILES:= $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
scripts/tolink.ml kernel/copcodes.ml
-export GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
# NB: all files in $(GENFILES) can be created initially, while
@@ -92,12 +96,9 @@ define diff
$(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef
-export MLSTATICFILES := \
- $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
-export MLFILES := \
- $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
-export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
include Makefile.common
@@ -276,3 +277,14 @@ ifdef COQ_CONFIGURED
else
@echo "Please run ./configure first" >&2; exit 1
endif
+
+# Useful to check that the exported variables are within the win32 limits
+
+printenv:
+ @env
+ @echo
+ @echo -n "Maxsize (win32 limit is 8k) : "
+ @env | wc -L
+ @echo -n "Total (win32 limit is 32k) : "
+ @env | wc -m
+
diff --git a/Makefile.build b/Makefile.build
index 41dfabbf..fe99f3b0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -36,10 +36,12 @@ endif
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
-ALLDEPS=$(addsuffix .d, \
+MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
+
+ALLDEPS:=$(addsuffix .d, \
$(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES)
+.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
# NOTA: the -include below will lauch the build of all .d. Some of them
# will _fail_ at first, this is to be expected (no grammar.cma initially).
@@ -82,12 +84,15 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)
OCAMLC += $(CAMLFLAGS)
OCAMLOPT += $(CAMLFLAGS)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
+COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
+COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= -slash $(LOCALINCLUDES)
define bestocaml
@@ -96,7 +101,7 @@ $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef
-CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
+CAMLP4DEPS=`LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<`
ifeq ($(CAMLP4),camlp5)
CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
else
@@ -169,10 +174,12 @@ CINCLUDES= -I $(CAMLHLIB)
# libcoqrun.a, dllcoqrun.so
+# NB: We used to do a ranlib after ocamlmklib, but it seems that
+# ocamlmklib is already doing it
+
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
cd $(dir $(LIBCOQRUN)) && \
$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
- $(RANLIB) $(LIBCOQRUN)
#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
@@ -201,12 +208,12 @@ states:: states/initial.coq
$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
$(STRIP) $@
$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
- $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@
+ $(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -544,9 +551,9 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST
ifeq ($(CAMLP4),camlp4)
tools/compat5.cmo: tools/compat5.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
tools/compat5b.cmo: tools/compat5b.mlp
- $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
else
tools/compat5.cmo: tools/compat5.ml
$(OCAMLC) -c $<
@@ -729,7 +736,7 @@ dev/printers.cma: | dev/printers.mllib.d
parsing/grammar.cma: | parsing/grammar.mllib.d
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
@@ -846,6 +853,12 @@ COND_OPTFLAGS= \
HACKMLI = $(if $(wildcard $)
+
+Theories:
+
+- Rendre transparent tous les theoremes prouvant {A}+{B}
+- Faire demarrer PolyList.nth a` l'indice 0
+ Renommer l'actuel nth en nth1 ??
+
+Doc:
+
+- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Documenter le filtrage sur les types inductifs avec let-ins (dont la
+ compatibilite V6)
+
+- Ajouter let dans les règles du CIC
+ -> FAIT, mais reste a documenter le let dans les inductifs
+ et les champs manifestes dans les Record
+- revoir le chapitre sur les tactiques utilisateur
+- faut-il mieux spécifier la sémantique de Simpl (??)
+
+- Préciser la clarification syntaxique de IntroPattern
+- preciser que Goal vient en dernier dans une clause pattern list et
+ qu'il doit apparaitre si il y a un "in"
+
+- Omega Time debranche mais Omega System et Omega Action remarchent ?
+- Ajout "Replace in" (mais TODO)
+- Syntaxe Conditional tac Rewrite marche, à documenter
+- Documenter Dependent Rewrite et CutRewrite ?
+- Ajouter les motifs sous-termes de ltac
+
+- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
+- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
+- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
+--> mettre à jour le CHANGES (vers la ligne 72)
+
+
diff --git a/checker/check.ml b/checker/check.ml
index bb42b949..237eb079 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* "
- echo "-with-ar "
- echo "-with-ranlib "
- printf "\tTells configure where to find gcc/ar/ranlib executables\n"
echo "-byte-only"
printf "\tCompiles only bytecode version of Coq\n"
echo "-debug"
@@ -119,10 +115,6 @@ best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
-gcc_exec=gcc
-ar_exec=ar
-ranlib_exec=ranlib
-
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
@@ -254,18 +246,6 @@ while : ; do
no) with_geoproof=false;;
esac
shift;;
- -with-cc|-with-gcc|--with-cc|--with-gcc)
- gcc_spec=yes
- gcc_exec=$2
- shift;;
- -with-ar|--with-ar)
- ar_spec=yes
- ar_exec=$2
- shift;;
- -with-ranlib|--with-ranlib)
- ranlib_spec=yes
- ranlib_exec=$2
- shift;;
-makecmd|--makecmd) makecmd="$2"
shift;;
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
@@ -292,17 +272,19 @@ case $DATEPGM in
"") echo "I can't find the program \"date\" in your path."
echo "Please give me the current date"
read COMPILEDATE;;
- *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;;
+ *) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
esac
# Architecture
case $arch_spec in
no)
- # First we test if we are running a Cygwin system
+ # First we test if we are running a Cygwin or Mingw/Msys system
if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
ARCH="win32"
CYGWIN=yes
+ elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
+ ARCH="win32"
else
# If not, we determine the architecture
if test -x /bin/uname ; then
@@ -437,12 +419,26 @@ if test ! -f "$CAMLC" ; then
exit 1
fi
-# Under Windows, OCaml only understands Windows filenames (C:\...)
-case $ARCH in
- win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
+# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
+# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
+
+mk_win_path () {
+ case $ARCH,$CYGWIN in
+ win32,yes) cygpath -m "$1" ;;
+ win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;;
+ *) echo "$1" ;;
+ esac
+}
+
+case $ARCH,$src_spec in
+ win32,yes) echo "Error: the -src option is currently not supported on Windows"
+ exit 1;;
+ win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
esac
-CAMLVERSION=`"$bytecamlc" -version`
+# Beware of the final \r in Win32
+CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
+CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
case $CAMLVERSION in
1.*|2.*|3.0*|3.10*|3.11.[01])
@@ -454,7 +450,7 @@ case $CAMLVERSION in
echo " Configuration script failed!"
exit 1
fi;;
- 3.11.2|3.12*)
+ 3.11.2|3.12*|4.*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -468,16 +464,9 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
# For coqmktop & bytecode compiler
-case $ARCH in
- win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
- CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
- *)
- CAMLLIB=`"$CAMLC" -where`
-esac
-
if [ "$coq_debug_flag" = "-g" ]; then
case $CAMLTAG in
- OCAML31*)
+ OCAML31*|OCAML4*)
# Compilation debug flag
coq_debug_flag_opt="-g"
;;
@@ -485,7 +474,7 @@ if [ "$coq_debug_flag" = "-g" ]; then
fi
# Native dynlink
-if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
+if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
HASNATDYNLINK=true
else
HASNATDYNLINK=false
@@ -520,7 +509,8 @@ esac
# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-if [ "$usecamlp5" = "yes" ]; then
+case $usecamlp5 in
+ yes)
CAMLP4=camlp5
CAMLP4MOD=gramlib
if [ "$camlp5dir" != "" ]; then
@@ -539,38 +529,47 @@ if [ "$usecamlp5" = "yes" ]; then
CAMLP4LIB=+site-lib/camlp5
FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
else
- echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
- echo "Configuration script failed!"
- exit 1
+ echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+ usecamlp5=no
fi
+esac
- camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
- case `$camlp4oexec -v 2>&1` in
- *4.0*|*5.00*)
+# If we're (still...) going to use Camlp5, let's check its version
+
+case $usecamlp5 in
+ yes)
+ camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
+ case `"$camlp4oexec" -v 2>&1` in
+ *"version 4.0"*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
esac
+esac
+
+# We might now try to use Camlp4, either by explicit choice or
+# by lack of proper Camlp5 installation
-else # let's use camlp4
+case $usecamlp5 in
+ no)
CAMLP4=camlp4
CAMLP4MOD=camlp4lib
CAMLP4LIB=+camlp4
FULLCAMLP4LIB=${CAMLLIB}/camlp4
if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
- echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+ echo "No Camlp4 installation found."
echo "Configuration script failed!"
exit 1
fi
camlp4oexec=${camlp4oexec}rf
- if [ "`$camlp4oexec 2>&1`" != "" ]; then
+ if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
echo "Error: $camlp4oexec not found or not executable."
echo "Configuration script failed!"
exit 1
fi
-fi
+esac
# do we have a native compiler: test of ocamlopt and its version
@@ -595,18 +594,17 @@ fi
# OS dependent libraries
-case $ARCH in
+OSDEPLIBS="-cclib -lunix"
+case $ARCH,$CYGWIN in
sun4*) OS=`uname -r`
case $OS in
5*) OS="Sun Solaris $OS"
- OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+ OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
*) OS="Sun OS $OS"
- OSDEPLIBS="-cclib -lunix"
esac;;
- win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix"
+ win32,yes) OS="Win32 (Cygwin)"
cflags="-mno-cygwin $cflags";;
- *) OSDEPLIBS="-cclib -lunix"
+ win32,*) OS="Win32 (MinGW)";;
esac
# lablgtk2 and CoqIDE
@@ -628,11 +626,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
echo "CoqIde disabled as requested."
else
case $lablgtkdir_spec in
- no)
- if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
+ no)
+ if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then
+ lablgtkdir_spec=yes
+ elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
lablgtkdir=${CAMLLIB}/lablgtk2
- elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
- lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
fi;;
yes)
if [ ! -f "$lablgtkdir/glib.mli" ]; then
@@ -656,10 +654,10 @@ else
else
echo "LablGtk2 found, native threads: native CoqIde will be available."
COQIDE=opt
- if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
+ if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration;
then
- cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
- IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+ cflags=$cflags" `pkg-config --cflags gtk-mac-integration`"
+ IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"'
IDEARCHFILE=ide/ide_mac_stubs.o
IDEARCHDEF=QUARTZ
elif [ "$ARCH" = "win32" ];
@@ -685,9 +683,6 @@ esac
# strip command
case $ARCH in
- win32)
- # true -> strip : it exists under cygwin !
- STRIPCOMMAND="strip";;
Darwin) if [ "$HASNATDYNLINK" = "true" ]
then
STRIPCOMMAND="true"
@@ -703,13 +698,6 @@ case $ARCH in
fi
esac
-# mktexlsr
-#MKTEXLSR=`which mktexlsr`
-#case $MKTEXLSR in
-# "") MKTEXLSR=true;;
-#esac
-
-# "
### Test if documentation can be compiled (latex, hevea)
if test "$with_doc" = "all"
@@ -727,26 +715,28 @@ fi
###########################################
# bindir, libdir, mandir, docdir, etc.
-case $src_spec in
- no) COQTOP=${COQSRC}
-esac
-
# OCaml only understand Windows filenames (C:\...)
case $ARCH in
- win32) COQTOP=`cygpath -m ${COQTOP}`
+ win32) COQSRC=`mk_win_path "$COQSRC"`
+ CAMLBIN=`mk_win_path "$CAMLBIN"`
+ CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
+esac
+
+case $src_spec in
+ no) COQTOP=${COQSRC}
esac
case $ARCH$CYGWIN in
win32)
- W32PREF='C:\\coq\\'
- bindir_def=${W32PREF}bin
- libdir_def=${W32PREF}lib
- configdir_def=${W32PREF}config
- datadir_def=${W32PREF}share
- mandir_def=${W32PREF}man
- docdir_def=${W32PREF}doc
- emacslib_def=${W32PREF}emacs
- coqdocdir_def=${W32PREF}latex;;
+ W32PREF='C:\coq\'
+ bindir_def="${W32PREF}bin"
+ libdir_def="${W32PREF}lib"
+ configdir_def="${W32PREF}config"
+ datadir_def="${W32PREF}share"
+ mandir_def="${W32PREF}man"
+ docdir_def="${W32PREF}doc"
+ emacslib_def="${W32PREF}emacs"
+ coqdocdir_def="${W32PREF}latex";;
*)
bindir_def=/usr/local/bin
libdir_def=/usr/local/lib/coq
@@ -755,7 +745,7 @@ case $ARCH$CYGWIN in
mandir_def=/usr/local/share/man
docdir_def=/usr/local/share/doc/coq
emacslib_def=/usr/local/share/emacs/site-lisp
- coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
+ coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
esac
emacs_def=emacs
@@ -764,7 +754,7 @@ case $bindir_spec/$prefix_spec/$local in
yes/*/*) BINDIR=$bindir ;;
*/yes/*) BINDIR=$prefix/bin ;;
*/*/true) BINDIR=$COQTOP/bin ;;
- *) printf "Where should I install the Coq binaries [$bindir_def]? "
+ *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def"
read BINDIR
case $BINDIR in
"") BINDIR=$bindir_def;;
@@ -781,7 +771,7 @@ case $libdir_spec/$prefix_spec/$local in
*) LIBDIR=$prefix/lib/coq ;;
esac ;;
*/*/true) LIBDIR=$COQTOP ;;
- *) printf "Where should I install the Coq library [$libdir_def]? "
+ *) printf "Where should I install the Coq library [%s]? " "$libdir_def"
read LIBDIR
libdir_spec=yes
case $LIBDIR in
@@ -790,11 +780,6 @@ case $libdir_spec/$prefix_spec/$local in
esac;;
esac
-case $libdir_spec in
- yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
- *) LIBDIR_OPTION="None";;
-esac
-
case $configdir_spec/$prefix_spec/$local in
yes/*/*) CONFIGDIR=$configdir;;
*/yes/*) configdir_spec=yes
@@ -804,7 +789,7 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
*/*/true) CONFIGDIR=$COQTOP/ide
configdir_spec=yes;;
- *) printf "Where should I install the Coqide configuration files [$configdir_def]? "
+ *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
read CONFIGDIR
case $CONFIGDIR in
"") CONFIGDIR=$configdir_def;;
@@ -812,17 +797,12 @@ case $configdir_spec/$prefix_spec/$local in
esac;;
esac
-case $configdir_spec in
- yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
- *) CONFIGDIR_OPTION="None";;
-esac
-
case $datadir_spec/$prefix_spec/$local in
yes/*/*) DATADIR=$datadir;;
*/yes/*) DATADIR=$prefix/share/coq;;
*/*/true) DATADIR=$COQTOP/ide
datadir_spec=yes;;
- *) printf "Where should I install the Coqide data files [$datadir_def]? "
+ *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def"
read DATADIR
case $DATADIR in
"") DATADIR=$datadir_def;;
@@ -830,17 +810,11 @@ case $datadir_spec/$prefix_spec/$local in
esac;;
esac
-case $datadir_spec in
- yes) DATADIR_OPTION="Some \"$DATADIR\"";;
- *) DATADIR_OPTION="None";;
-esac
-
-
case $mandir_spec/$prefix_spec/$local in
yes/*/*) MANDIR=$mandir;;
*/yes/*) MANDIR=$prefix/share/man ;;
*/*/true) MANDIR=$COQTOP/man ;;
- *) printf "Where should I install the Coq man pages [$mandir_def]? "
+ *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def"
read MANDIR
case $MANDIR in
"") MANDIR=$mandir_def;;
@@ -852,7 +826,7 @@ case $docdir_spec/$prefix_spec/$local in
yes/*/*) DOCDIR=$docdir;;
*/yes/*) DOCDIR=$prefix/share/doc/coq;;
*/*/true) DOCDIR=$COQTOP/doc;;
- *) printf "Where should I install the Coq documentation [$docdir_def]? "
+ *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
read DOCDIR
case $DOCDIR in
"") DOCDIR=$docdir_def;;
@@ -868,7 +842,7 @@ case $emacslib_spec/$prefix_spec/$local in
*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) EMACSLIB=$COQTOP/tools/emacs ;;
- *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
+ *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def"
read EMACSLIB
case $EMACSLIB in
"") EMACSLIB=$emacslib_def;;
@@ -884,7 +858,7 @@ case $coqdocdir_spec/$prefix_spec/$local in
*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
esac ;;
*/*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
- *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
+ *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def"
read COQDOCDIR
case $COQDOCDIR in
"") COQDOCDIR=$coqdocdir_def;;
@@ -914,14 +888,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
esac
# case $emacs_spec in
-# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
+# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def"
# read EMACS
# case $EMACS in
-# "") EMACS=$emacs_def;;
+# "") EMACS="$emacs_def";;
# *) true;;
# esac;;
-# yes) EMACS=$emacs;;
+# yes) EMACS="$emacs";;
# esac
@@ -1016,51 +990,63 @@ config_template="$COQSRC/config/Makefile.template"
### After this line, be careful when using variables,
### since some of them (e.g. $COQSRC) will be escaped
-
-# An escaped version of a variable
-escape_var () {
-"$ocamlexec" 2>&1 1>/dev/null < "$config_file"
+cat << END_OF_MAKEFILE > $config_file
+###### config/Makefile : Configuration file for Coq ##############
+# #
+# This file is generated by the script "configure" #
+# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! #
+# If something is wrong below, then rerun the script "configure" #
+# with the good options (see the file INSTALL). #
+# #
+##################################################################
+
+#Variable used to detect whether ./configure has run successfully.
+COQ_CONFIGURED=yes
+
+# Local use (no installation)
+LOCAL=$local
+
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
+$BUILDLDPATH
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+# do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="$BINDIR"
+COQLIBINSTALL="$LIBDIR"
+CONFIGDIR="$CONFIGDIR"
+DATADIR="$DATADIR"
+MANDIR="$MANDIR"
+DOCDIR="$DOCDIR"
+EMACSLIB="$EMACSLIB"
+EMACS=$EMACS
+
+# Path to Coq distribution
+COQSRC="$COQSRC"
+VERSION=$VERSION
+
+# Ocaml version number
+CAMLVERSION=$CAMLTAG
+
+# Ocaml libraries
+CAMLLIB="$CAMLLIB"
+
+# Ocaml .h directory
+CAMLHLIB="$CAMLLIB"
+
+# Camlp4 : flavor, binaries, libraries ...
+# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
+# NB : avoid using CAMLP4LIB (conflict under Windows)
+CAMLP4BIN="$CAMLP4BIN"
+CAMLP4=$CAMLP4
+CAMLP4O=$camlp4oexec
+CAMLP4COMPAT=$CAMLP4COMPAT
+MYCAMLP4LIB="$CAMLP4LIB"
+
+# LablGTK
+COQIDEINCLUDES=$LABLGTKINCLUDES
+
+# Objective-Caml compile command
+OCAML="$ocamlexec"
+OCAMLC="$bytecamlc"
+OCAMLMKLIB="$ocamlmklibexec"
+OCAMLOPT="$nativecamlc"
+OCAMLDEP="$ocamldepexec"
+OCAMLDOC="$ocamldocexec"
+OCAMLLEX="$ocamllexexec"
+OCAMLYACC="$ocamlyaccexec"
+
+# Caml link command and Caml make top command
+CAMLLINK="$bytecamlc"
+CAMLOPTLINK="$nativecamlc"
+CAMLMKTOP="$ocamlmktopexec"
+
+# Caml flags
+CAMLFLAGS=-rectypes $coq_annotate_flag
+
+# Compilation debug flags
+CAMLDEBUG=$coq_debug_flag
+CAMLDEBUGOPT=$coq_debug_flag_opt
+
+# User compilation flag
+USERFLAGS=
+
+# Flags for GCC
+CFLAGS=$cflags
+
+# Compilation profile flag
+CAMLTIMEPROF=$coq_profile_flag
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=$best_compiler
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=$ARCH
+HASNATDYNLINK=$NATDYNLINKFLAG
+
+# Supplementary libs for some systems, currently:
+# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+# . others : -cclib -lunix
+OSDEPLIBS=$OSDEPLIBS
+
+# executable files extension, currently:
+# Unix systems:
+# Win32 systems : .exe
+EXE=$EXE
+DLLEXT=$DLLEXT
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR="$COQDOCDIR"
+
+#the command STRIP
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+STRIP=$STRIPCOMMAND
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=$COQIDE
+IDEOPTFLAGS=$IDEARCHFLAGS
+IDEOPTDEPS=$IDEARCHFILE
+IDEOPTINT=$IDEARCHDEF
+
+# Defining REVISION
+CHECKEDOUT=$checkedout
+
+# Option to control compilation and installation of the documentation
+WITHDOC=$with_doc
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
+END_OF_MAKEFILE
chmod a-w "$config_file"
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index b3edd7d0..f54df8a8 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* \(.*\)$/\1\2/
+s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3116cbf2..0038e78a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* try pp(pr_ltype x) with e -> pp (str (Printexc.to_string
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
-let ppbigint n = pp (Bigint.pr_bigint n);;
+let ppbigint n = pp (str (Bigint.to_string n));;
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Intset.elements l))
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
deleted file mode 100644
index 707ee824..00000000
--- a/doc/refman/RefMan-sch.tex
+++ /dev/null
@@ -1,418 +0,0 @@
-\chapter{Proof schemes}
-
-\section{Generation of induction principles with {\tt Scheme}}
-\label{Scheme}
-\index{Schemes}
-\comindex{Scheme}
-
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts. Its syntax follows the schema:
-\begin{quote}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
- {\sort$_m$}}
-
- Same as before but defines a non-dependent elimination principle more
- natural in case of inductively defined relations.
-
-\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
-
- Tries to generate a boolean equality and a proof of the
- decidability of the usual equality. If \ident$_i$ involves
- some other inductive types, their equality has to be defined first.
-
-\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\\
- with Induction for {\ident$_m$} Sort
- {\sort$_m$}}
-
- If you do not provide the name of the schemes, they will be automatically
- computed from the sorts involved (works also with Minimality).
-
-\end{Variants}
-\label{Scheme-examples}
-
-\firstexample
-\example{Induction scheme for \texttt{tree} and \texttt{forest}}
-
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-
-\begin{coq_eval}
-Reset Initial.
-Variables A B : Set.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | leaf : B -> forest
- | cons : tree -> forest -> forest.
-
-Scheme tree_forest_rec := Induction for tree Sort Set
- with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_forest\_rec}:
-
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt forest\_tree\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\example{Predicates {\tt odd} and {\tt even} on naturals}
-
-Let {\tt odd} and {\tt even} be inductively defined as:
-
-% Reset Initial.
-\begin{coq_eval}
-Open Scope nat_scope.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
- oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
- | evenO : even 0
- | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-
-The following command generates a powerful elimination
-principle:
-
-\begin{coq_example}
-Scheme odd_even := Minimality for odd Sort Prop
- with even_odd := Minimality for even Sort Prop.
-\end{coq_example}
-
-The type of {\tt odd\_even} for instance will be:
-
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection{Automatic declaration of schemes}
-\comindex{Set Equality Schemes}
-\comindex{Set Elimination Schemes}
-
-It is possible to deactivate the automatic declaration of the induction
- principles when defining a new inductive type with the
- {\tt Unset Elimination Schemes} command. It may be
-reactivated at any time with {\tt Set Elimination Schemes}.
-\\
-
-You can also activate the automatic declaration of those boolean equalities
-(see the second variant of {\tt Scheme}) with the {\tt Set Equality Schemes}
- command. However you have to be careful with this option since
-\Coq~ may now reject well-defined inductive types because it cannot compute
-a boolean equality for them.
-
-\subsection{\tt Combined Scheme}
-\label{CombinedScheme}
-\comindex{Combined Scheme}
-
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-\begin{quote}
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
-\end{quote}
-where
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-built from the common premises of the principles and concluded by the
-conjunction of their conclusions.
-
-\Example
-We can define the induction principles for trees and forests using:
-\begin{coq_example}
-Scheme tree_forest_ind := Induction for tree Sort Prop
- with forest_tree_ind := Induction for forest Sort Prop.
-\end{coq_example}
-
-Then we can build the combined induction principle which gives the
-conjunction of the conclusions of each individual principle:
-\begin{coq_example}
-Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
-\end{coq_example}
-
-The type of {\tt tree\_forest\_mutrec} will be:
-\begin{coq_example}
-Check tree_forest_mutind.
-\end{coq_example}
-
-\section{Generation of induction principles with {\tt Functional Scheme}}
-\label{FunScheme}
-\comindex{Functional Scheme}
-
-The {\tt Functional Scheme} command is a high-level experimental
-tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions. Its
-syntax follows the schema:
-\begin{quote}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} \dots\ \\
- with {\ident$_m$} := Induction for {\ident'$_m$} Sort
- {\sort$_m$}}
-\end{quote}
-where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-\Rem
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-\firstexample
-\example{Induction scheme for \texttt{div2}}
-\label{FunScheme-examples}
-
-We define the function \texttt{div2} as follows:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Require Import Arith.
-Fixpoint div2 (n:nat) : nat :=
- match n with
- | O => 0
- | S O => 0
- | S (S n') => S (div2 n')
- end.
-\end{coq_example*}
-
-The definition of a principle of induction corresponding to the
-recursive structure of \texttt{div2} is defined by the command:
-
-\begin{coq_example}
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-\end{coq_example}
-
-You may now look at the type of {\tt div2\_ind}:
-
-\begin{coq_example}
-Check div2_ind.
-\end{coq_example}
-
-We can now prove the following lemma using this principle:
-
-\begin{coq_example*}
-Lemma div2_le' : forall n:nat, div2 n <= n.
-intro n.
- pattern n , (div2 n).
-\end{coq_example*}
-
-\begin{coq_example}
-apply div2_ind; intros.
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-simpl; auto with arith.
-Qed.
-\end{coq_example*}
-
-We can use directly the \texttt{functional induction}
-(\ref{FunInduction}) tactic instead of the pattern/apply trick:
-\tacindex{functional induction}
-
-\begin{coq_example*}
-Reset div2_le'.
-Lemma div2_le : forall n:nat, div2 n <= n.
-intro n.
-\end{coq_example*}
-
-\begin{coq_example}
-functional induction (div2 n).
-\end{coq_example}
-
-\begin{coq_example*}
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-\end{coq_example*}
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (see Section~\ref{Function}) and by
-using \texttt{Functional Scheme} after a normal definition using
-\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
-details.
-
-
-\example{Induction scheme for \texttt{tree\_size}}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-We define trees by the following mutual inductive type:
-
-\begin{coq_example*}
-Variable A : Set.
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | empty : forest
- | cons : tree -> forest -> forest.
-\end{coq_example*}
-
-We define the function \texttt{tree\_size} that computes the size
-of a tree or a forest. Note that we use \texttt{Function} which
-generally produces better principles.
-
-\begin{coq_example*}
-Function tree_size (t:tree) : nat :=
- match t with
- | node A f => S (forest_size f)
- end
- with forest_size (f:forest) : nat :=
- match f with
- | empty => 0
- | cons t f' => (tree_size t + forest_size f')
- end.
-\end{coq_example*}
-
-\Rem \texttt{Function} generates itself non mutual induction
-principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
-
-\begin{coq_example}
-Check tree_size_ind.
-\end{coq_example}
-
-The definition of mutual induction principles following the recursive
-structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
-by the command:
-
-\begin{coq_example*}
-Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-with forest_size_ind2 := Induction for forest_size Sort Prop.
-\end{coq_example*}
-
-You may now look at the type of {\tt tree\_size\_ind2}:
-
-\begin{coq_example}
-Check tree_size_ind2.
-\end{coq_example}
-
-\section{Generation of inversion principles with \tt Derive Inversion}
-\label{Derive-Inversion}
-\comindex{Derive Inversion}
-
-The syntax of {\tt Derive Inversion} follows the schema:
-\begin{quote}
-{\tt Derive Inversion {\ident} with forall
- $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
-\end{quote}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-\tacindex{inversion \dots\ using}
-Let $I$ be an inductive predicate and $\vec{x}$ the variables
-occurring in $\vec{t}$. This command generates and stocks the
-inversion lemma for the sort \sort~ corresponding to the instance
-$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
-global} environment. When applied, it is equivalent to having inverted
-the instance with the tactic {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{inversion}
- replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
- $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
- \comindex{Derive Dependent Inversion\_clear}
- When applied, it is equivalent to having
- inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\Example
-
-Let us consider the relation \texttt{Le} over natural numbers and the
-following variable:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
- | LeO : forall n:nat, Le 0 n
- | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-\end{coq_example*}
-
-To generate the inversion lemma for the instance
-\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do:
-
-\begin{coq_example*}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example*}
-
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-Then we can use the proven inversion lemma:
-
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ee101c8..833b5c4c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -400,6 +400,7 @@ through the Require Import command.
theories/Lists/List.v
theories/Lists/ListSet.v
theories/Lists/SetoidList.v
+ theories/Lists/SetoidPermutation.v
theories/Lists/Streams.v
theories/Lists/StreamMemo.v
theories/Lists/ListTactics.v
@@ -523,7 +524,10 @@ through the Require Import command.
theories/Reals/Rsigma.v
theories/Reals/R_sqr.v
theories/Reals/Rtrigo_fun.v
+ theories/Reals/Rtrigo1.v
theories/Reals/Rtrigo.v
+ theories/Reals/Ratan.v
+ theories/Reals/Machin.v
theories/Reals/SplitAbsolu.v
theories/Reals/SplitRmult.v
theories/Reals/Alembert.v
@@ -544,6 +548,8 @@ through the Require Import command.
theories/Reals/Ranalysis2.v
theories/Reals/Ranalysis3.v
theories/Reals/Ranalysis4.v
+ theories/Reals/Ranalysis5.v
+ theories/Reals/Ranalysis_reg.v
theories/Reals/Rcomplete.v
theories/Reals/RiemannInt.v
theories/Reals/RiemannInt_SF.v
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a34e5ebe..470bd5b4 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
let path = match status.Interface.status_path with
- | None -> ""
- | Some p -> " in " ^ p
+ | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+ | _ :: l -> " in " ^ String.concat "." l
in
let name = match status.Interface.status_proofname with
| None -> ""
@@ -2449,13 +2449,13 @@ let main files =
try configure ~apply:update_notebook_pos ()
with _ -> flash_info "Cannot save preferences"
end;
- reset_revert_timer ()) ~stock:`PREFERENCES;
+ reset_revert_timer ()) ~accel:"," ~stock:`PREFERENCES;
(* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
GAction.add_actions view_actions [
GAction.add_action "View" ~label:"_View";
- GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
+ GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("Left") ~stock:`GO_BACK
~callback:(fun _ -> session_notebook#previous_page ());
- GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
+ GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("Right") ~stock:`GO_FORWARD
~callback:(fun _ -> session_notebook#next_page ());
GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
~active:(!current.show_toolbar) ~callback:
@@ -2624,6 +2624,7 @@ let main files =
Coqide_ui.ui_m#insert_action_group windows_actions 0;
Coqide_ui.ui_m#insert_action_group help_actions 0;
w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
+ GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
if Coq_config.gtk_platform <> `QUARTZ
then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 57158a6a..18df1f6a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
#include
#include
-#include
+#include
GtkOSXApplication *theApp;
value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
@@ -76,10 +76,10 @@ CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
caml_register_generational_global_root(&about_item);
/* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
- about_grp = gtk_osxapplication_add_app_menu_group(theApp);
- pref_grp = gtk_osxapplication_add_app_menu_group(theApp);
- gtk_osxapplication_add_app_menu_item(theApp,about_grp,check_cast(GTK_MENU_ITEM,about_item));
- gtk_osxapplication_add_app_menu_item(theApp,pref_grp,check_cast(GTK_MENU_ITEM,pref_item));
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
+ gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
+ gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
gtk_osxapplication_ready(theApp);
CAMLreturn(Val_unit);
}
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index b79d6469..697e7f4f 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* []
+| (lg, rg) :: l ->
+ let inner = flatten l in
+ List.rev_append lg inner @ rg
+
let display mode (view:GText.view) goals hints evars =
let () = view#buffer#set_text "" in
match goals with
| None -> ()
(* No proof in progress *)
- | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
- (* A proof has been finished, but not concluded *)
- begin match evars with
- | Some evs when evs <> [] ->
+ | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+ let bg = flatten (List.rev bg) in
+ let evars = match evars with None -> [] | Some evs -> evs in
+ begin match (bg, evars) with
+ | [], [] ->
+ view#buffer#insert "No more subgoals."
+ | [], _ :: _ ->
+ (* A proof has been finished, but not concluded *)
view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
let iter evar =
let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
view#buffer#insert msg
in
- List.iter iter evs
- | _ ->
- view#buffer#insert "No more subgoals."
+ List.iter iter evars
+ | _, _ ->
+ (* No foreground proofs, but still unfocused ones *)
+ view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+ let iter goal =
+ let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+ view#buffer#insert msg
+ in
+ List.iter iter bg
end
- | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
- (* No foreground proofs, but still unfocused ones *)
- view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
- let iter goal =
- let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
- view#buffer#insert msg
- in
- List.iter iter bg
| Some { Interface.fg_goals = fg } ->
mode view fg hints
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a208ad0e..164c837a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* /C_anonical Structure/" "")
-; (gtk_accel_path "/M_odule Type/" "")
-; (gtk_accel_path "/c_ompute/" "")
-; (gtk_accel_path "/Templates/_E.../" "")
-(gtk_accel_path "/Templates/match" "c")
-; (gtk_accel_path "/D_erive Inversion/" "")
-; (gtk_accel_path "/Queries/Check" "F3")
-; (gtk_accel_path "/i_dtac/" "")
-; (gtk_accel_path "/L_oad/" "")
-; (gtk_accel_path "/a_ssert/" "")
-; (gtk_accel_path "/f_irstorder using/" "")
-; (gtk_accel_path "/s_olve/" "")
-; (gtk_accel_path "/Tactics/_l.../" "")
-(gtk_accel_path "/Templates/Inductive" "i")
-; (gtk_accel_path "/a_ssert (__:__)/" "")
-; (gtk_accel_path "/T_est Printing Synth/" "")
-; (gtk_accel_path "/Templates/_R.../" "")
-; (gtk_accel_path "/Help/Browse Coq Library" "")
-; (gtk_accel_path "/U_nset Extraction Optimize/" "")
-; (gtk_accel_path "/s_imple inversion/" "")
-(gtk_accel_path "/Edit/Copy" "c")
-; (gtk_accel_path "/E_xtract Inductive/" "")
-(gtk_accel_path "/Edit/Cut" "x")
-; (gtk_accel_path "/i_nfo/" "")
-; (gtk_accel_path "/R_emove Printing If/" "")
-; (gtk_accel_path "/e_apply/" "")
-; (gtk_accel_path "/F_ixpoint/" "")
-; (gtk_accel_path "/c_hange __ in/" "")
-; (gtk_accel_path "/l_apply/" "")
-; (gtk_accel_path "/s_imple induction/" "")
-; (gtk_accel_path "/f_ail/" "")
-; (gtk_accel_path "/e_lim/" "")
-; (gtk_accel_path "/r_ewrite <- __ in/" "")
-; (gtk_accel_path "/A_dd Printing Let/" "")
-; (gtk_accel_path "/T_ransparent/" "")
-; (gtk_accel_path "/Tactics/_d.../" "")
-(gtk_accel_path "/Tactics/Wizard" "dollar")
+; (gtk_accel_path "/Templates/Template Read Module" "")
+; (gtk_accel_path "/Tactics/Tactic pattern" "")
+(gtk_accel_path "/Templates/Definition" "d")
+; (gtk_accel_path "/Templates/Template Program Lemma" "")
+(gtk_accel_path "/Templates/Lemma" "l")
+; (gtk_accel_path "/Templates/Template Fact" "")
+(gtk_accel_path "/Tactics/auto" "a")
+; (gtk_accel_path "/Tactics/Tactic fold" "")
+; (gtk_accel_path "/Help/About Coq" "")
+; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
+; (gtk_accel_path "/Templates/Template Hypothesis" "")
+; (gtk_accel_path "/Tactics/Tactic repeat" "")
+; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "")
+; (gtk_accel_path "/Templates/Template Add Printing Constructor" "")
; (gtk_accel_path "/Windows/Detach View" "")
-; (gtk_accel_path "/T_heorem/" "")
-(gtk_accel_path "/Templates/Scheme" "s")
-; (gtk_accel_path "/R_emark/" "")
-; (gtk_accel_path "/Compile/Compile" "")
-; (gtk_accel_path "/A_dd Relation/" "")
-; (gtk_accel_path "/r_ename __ into/" "")
-; (gtk_accel_path "/File/Save as" "")
-; (gtk_accel_path "/f_irstorder/" "")
-; (gtk_accel_path "/G_rammar/" "")
-; (gtk_accel_path "/f_irstorder with/" "")
-; (gtk_accel_path "/r_ed/" "")
-; (gtk_accel_path "/D_efinition/" "")
-; (gtk_accel_path "/R_equire Import/" "")
-; (gtk_accel_path "/d_iscriminate/" "")
-; (gtk_accel_path "/i_ntro after/" "")
-; (gtk_accel_path "/Export/Latex" "")
-; (gtk_accel_path "/j_p/" "")
-; (gtk_accel_path "/a_uto with/" "")
-; (gtk_accel_path "/S_ection/" "")
-; (gtk_accel_path "/r_ewrite/" "")
-; (gtk_accel_path "/Export/Html" "")
-; (gtk_accel_path "/Tactics/_i.../" "")
-; (gtk_accel_path "/a_utorewrite/" "")
-; (gtk_accel_path "/F_ocus/" "")
-; (gtk_accel_path "/Templates/_O.../" "")
-; (gtk_accel_path "/l_azy in/" "")
-; (gtk_accel_path "/d_ependent inversion__clear __ with/" "")
-; (gtk_accel_path "/c_utrewrite/" "")
-(gtk_accel_path "/Edit/Undo" "u")
-; (gtk_accel_path "/c_onstructor __ with/" "")
-; (gtk_accel_path "/r_ing/" "")
-; (gtk_accel_path "/d_ependent rewrite <-/" "")
-; (gtk_accel_path "/e_limtype/" "")
-(gtk_accel_path "/Tactics/simpl" "s")
-; (gtk_accel_path "/H_int/" "")
-; (gtk_accel_path "/H_int Rewrite/" "")
-; (gtk_accel_path "/V_ariable/" "")
-; (gtk_accel_path "/U_nset Implicit Arguments/" "")
-; (gtk_accel_path "/s_implify__eq/" "")
-; (gtk_accel_path "/Compile/Next error" "F7")
-; (gtk_accel_path "/Edit/Edit" "")
-; (gtk_accel_path "/S_et Extraction Optimize/" "")
-; (gtk_accel_path "/H_ypothesis/" "")
-; (gtk_accel_path "/E_nd Silent./" "")
-; (gtk_accel_path "/S_yntax/" "")
-; (gtk_accel_path "/d_ecide equality/" "")
-; (gtk_accel_path "/O_paque/" "")
-; (gtk_accel_path "/Templates/_T.../" "")
-; (gtk_accel_path "/Tactics/_a.../" "")
-; (gtk_accel_path "/Templates/_G.../" "")
-; (gtk_accel_path "/c_ase/" "")
-(gtk_accel_path "/Navigation/Backward" "Up")
-; (gtk_accel_path "/C_oFixpoint/" "")
-; (gtk_accel_path "/P_rogram Fixpoint/" "")
-; (gtk_accel_path "/d_ependent inversion__clear/" "")
-; (gtk_accel_path "/c_ase __ with/" "")
-; (gtk_accel_path "/a_ssumption/" "")
-; (gtk_accel_path "/t_ransitivity/" "")
-; (gtk_accel_path "/i_ntros until/" "")
-; (gtk_accel_path "/s_plit/" "")
-; (gtk_accel_path "/e_xists/" "")
-(gtk_accel_path "/Templates/Theorem" "t")
-; (gtk_accel_path "/Navigation/Navigation" "")
-; (gtk_accel_path "/H_int Unfold/" "")
-; (gtk_accel_path "/I_mplicit Arguments/" "")
-; (gtk_accel_path "/Help/Help" "")
-; (gtk_accel_path "/d_ecompose sum/" "")
-; (gtk_accel_path "/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "")
-; (gtk_accel_path "/Te_mplates/" "")
-(gtk_accel_path "/Edit/Find in buffer" "f")
-; (gtk_accel_path "/r_eplace __ with/" "")
-(gtk_accel_path "/Tactics/omega" "o")
-; (gtk_accel_path "/S_cheme/" "")
-; (gtk_accel_path "/L_emma/" "")
-; (gtk_accel_path "/i_nversion__clear __ in/" "")
-; (gtk_accel_path "/E_xtraction Inline/" "")
-; (gtk_accel_path "/S_yntactic Definition/" "")
-; (gtk_accel_path "/i_nstantiate (__:=__)/" "")
-; (gtk_accel_path "/C_hapter/" "")
-; (gtk_accel_path "/Templates/_L.../" "")
-; (gtk_accel_path "/Tactics/_f.../" "")
-; (gtk_accel_path "/Queries/Queries" "")
-; (gtk_accel_path "/T_est Printing Wildcard/" "")
-(gtk_accel_path "/File/Open" "o")
-; (gtk_accel_path "/f_old __ in/" "")
-(gtk_accel_path "/Navigation/Go to" "Right")
+; (gtk_accel_path "/Tactics/Tactic inversion" "")
+; (gtk_accel_path "/Templates/Template Write State" "")
; (gtk_accel_path "/Export/Export to" "")
-; (gtk_accel_path "/c_ongruence/" "")
-; (gtk_accel_path "/c_learbody/" "")
-(gtk_accel_path "/File/Close buffer" "w")
-; (gtk_accel_path "/a_pply/" "")
-; (gtk_accel_path "/Queries/SearchAbout" "F2")
-; (gtk_accel_path "/i_ntro/" "")
-; (gtk_accel_path "/H_int Immediate/" "")
-; (gtk_accel_path "/p_ose __:=__)/" "")
-; (gtk_accel_path "/U_nset Undo/" "")
-; (gtk_accel_path "/Tactics/_s.../" "")
-; (gtk_accel_path "/P_rogram Definition/" "")
-; (gtk_accel_path "/R_equire/" "")
-; (gtk_accel_path "/c_ompare/" "")
-; (gtk_accel_path "/s_ymmetry in/" "")
-(gtk_accel_path "/Display/Display coercions" "c")
-(gtk_accel_path "/Navigation/Previous" "less")
-(gtk_accel_path "/Display/Display all low-level contents" "l")
-; (gtk_accel_path "/C_oercion Local/" "")
-; (gtk_accel_path "/f_ix __ with/" "")
-; (gtk_accel_path "/A_dd ML Path/" "")
-; (gtk_accel_path "/A_xiom/" "")
-; (gtk_accel_path "/Templates/Templates" "")
-; (gtk_accel_path "/a_bstract/" "")
-; (gtk_accel_path "/Edit/Clear Undo Stack" "")
-(gtk_accel_path "/File/New" "n")
-; (gtk_accel_path "/Tactics/_hnf/" "")
-; (gtk_accel_path "/d_o/" "")
-; (gtk_accel_path "/E_xtract Constant/" "")
-; (gtk_accel_path "/E_nd/" "")
-; (gtk_accel_path "/Templates/_Qed./" "")
-; (gtk_accel_path "/A_dd Rec ML Path/" "")
-; (gtk_accel_path "/Templates/_D.../" "")
-(gtk_accel_path "/Navigation/Hide" "h")
-; (gtk_accel_path "/c_ofix/" "")
-; (gtk_accel_path "/_Try Tactics/" "")
-; (gtk_accel_path "/S_et Printing Wildcard/" "")
-; (gtk_accel_path "/i_nversion__clear/" "")
-; (gtk_accel_path "/Templates/_V.../" "")
+(gtk_accel_path "/Tactics/auto with *" "asterisk")
+; (gtk_accel_path "/Tactics/Tactic inversion--clear" "")
+; (gtk_accel_path "/Templates/Template Implicit Arguments" "")
+(gtk_accel_path "/Edit/Find backwards" "b")
+; (gtk_accel_path "/Edit/Copy" "c")
+; (gtk_accel_path "/Tactics/Tactic inversion -- using" "")
+(gtk_accel_path "/View/Previous tab" "Left")
+; (gtk_accel_path "/Tactics/Tactic change -- in" "")
+; (gtk_accel_path "/Tactics/Tactic jp" "")
+; (gtk_accel_path "/Tactics/Tactic red" "")
+; (gtk_accel_path "/Templates/Template Coercion" "")
+; (gtk_accel_path "/Templates/Template CoFixpoint" "")
+; (gtk_accel_path "/Tactics/Tactic intros until" "")
+; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "")
+; (gtk_accel_path "/Tactics/Tactic eapply" "")
+; (gtk_accel_path "/View/View" "")
+; (gtk_accel_path "/Tactics/Tactic change" "")
+; (gtk_accel_path "/Tactics/Tactic firstorder using" "")
+; (gtk_accel_path "/Tactics/Tactic decompose sum" "")
+; (gtk_accel_path "/Tactics/Tactic cut" "")
+; (gtk_accel_path "/Templates/Template Remove Printing Let" "")
+; (gtk_accel_path "/Templates/Template Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compute in" "")
+; (gtk_accel_path "/Queries/Locate" "")
+; (gtk_accel_path "/Templates/Template Save." "")
+; (gtk_accel_path "/Templates/Template Canonical Structure" "")
+; (gtk_accel_path "/Tactics/Tactic compare" "")
+; (gtk_accel_path "/Templates/Template Next Obligation" "")
+(gtk_accel_path "/View/Display notations" "n")
+; (gtk_accel_path "/Tactics/Tactic fail" "")
+; (gtk_accel_path "/Tactics/Tactic left" "")
+(gtk_accel_path "/Edit/Undo" "u")
+(gtk_accel_path "/Tactics/eauto with *" "