Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

8 files changed, 74 insertions, 28 deletions

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 06b4e028..f84d8f58 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *)
+(* $Id: FSetDecide.v 13199 2010-06-25 22:36:22Z letouzey $ *)
 
 (**************************************************************)
 (* FSetDecide.v                                               *)
@@ -346,6 +346,19 @@ the above form:
     (** ** Generic Tactics
         We begin by defining a few generic, useful tactics. *)
 
+    (** remove logical hypothesis inter-dependencies (fix #2136). *)
+
+    Ltac no_logical_interdep :=
+      match goal with
+        | H : ?P |- _ =>
+          match type of P with
+            | Prop =>
+              match goal with H' : context [ H ] |- _ => clear dependent H' end
+            | _ => fail
+          end; no_logical_interdep
+        | _ => idtac
+      end.
+
     (** [if t then t1 else t2] executes [t] and, if it does not
         fail, then [t1] will be applied to all subgoals
         produced.  If [t] fails, then [t2] is executed. *)
@@ -405,7 +418,7 @@ the above form:
         propositions of interest. *)
 
     Inductive FSet_elt_Prop : Prop -> Prop :=
-    | eq_Prop : forall (S : Set) (x y : S),
+    | eq_Prop : forall (S : Type) (x y : S),
         FSet_elt_Prop (x = y)
     | eq_elt_prop : forall x y,
         FSet_elt_Prop (E.eq x y)
@@ -660,6 +673,9 @@ the above form:
   Ltac fsetdec :=
     (** We first unfold any occurrences of [iff]. *)
     unfold iff in *;
+    (** We remove dependencies to logical hypothesis. This way,
+        later "clear" will work nicely (see bug #2136) *)
+    no_logical_interdep;
     (** We fold occurrences of [not] because it is better for
         [intros] to leave us with a goal of [~ P] than a goal of
         [False]. *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 3dc6385d..5f18edcd 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
+(*i $Id: Notations.v 12271 2009-08-11 10:29:45Z herbelin $ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
@@ -68,13 +68,13 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
 (** Notations for sigma-types or subsets *)
 
 Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x  |  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x  |  P  & Q }" (at level 0, x at level 99).
 
 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  |  P  & Q }" (at level 0, x at level 99).
 
-Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
 
 Delimit Scope type_scope with type.
 Delimit Scope core_scope with core.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 2d7e2159..48b4568d 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 11741 2009-01-03 14:34:39Z herbelin $ i*)
+(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
 
 Require Import Notations.
 Require Import Logic.
@@ -174,3 +174,20 @@ Tactic Notation "now" tactic(t) := t; easy.
 
 (** A tactic to document or check what is proved at some point of a script *)
 Ltac now_show c := change c.
+
+(** Clear an hypothesis and its dependencies *)
+
+Tactic Notation "clear" "dependent" hyp(h) :=
+ let rec depclear h :=
+  clear h ||
+  match goal with
+   | H : context [ h ] |- _ => depclear H; depclear h
+  end ||
+  fail "hypothesis to clear is used in the conclusion (maybe indirectly)"
+ in depclear h.
+
+(** Revert an hypothesis and its dependencies :
+    this is actually generalize dependent... *)
+
+Tactic Notation "revert" "dependent" hyp(h) :=
+ generalize dependent h.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index a72283d9..c015854e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
+(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*)
 
 Require Import Le Gt Minus Min Bool.
 
@@ -1081,11 +1081,11 @@ Section Map.
 
   (** [flat_map] *)
 
-  Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : 
-    list B :=
+  Definition flat_map (f:A -> list B) :=
+    fix flat_map (l:list A) {struct l} : list B :=
     match l with
       | nil => nil
-      | cons x t => (f x)++(flat_map f t)
+      | cons x t => (f x)++(flat_map t)
     end.
   
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 21f2513f..f01cbbc5 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: BigQ.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*)
 
 Require Import Field Qfield BigN BigZ QSig QMake.
 
@@ -44,6 +44,11 @@ Delimit Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with BigQ.t.
 
+(* Allow nice printing of rational numerals, either as (Qz 1234)
+   or as (Qq 1234 5678) *)
+Arguments Scope BigQ.Qz [bigZ_scope].
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].			     
+			     
 Infix "+" := BigQ.add : bigQ_scope.
 Infix "-" := BigQ.sub : bigQ_scope.
 Notation "- x" := (BigQ.opp x) : bigQ_scope.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 78cf2892..0b6d1cfe 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith_base.v 11301 2008-08-04 19:41:18Z herbelin $ i*)
+(*i $Id: QArith_base.v 13215 2010-06-29 09:31:45Z letouzey $ i*)
 
 Require Export ZArith.
 Require Export ZArithRing.
@@ -157,16 +157,15 @@ Qed.
 
 (** We now consider [Q] seen as a setoid. *)
 
-Definition Q_Setoid : Setoid_Theory Q Qeq.
-Proof.
- split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
-Qed.
+Add Relation Q Qeq
+  reflexivity proved by Qeq_refl
+  symmetry proved by Qeq_sym
+  transitivity proved by Qeq_trans
+as Q_Setoid.
 
-Add Setoid Q Qeq Q_Setoid as Qsetoid.
-
-Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
-Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
+Hint Resolve Qeq_refl : qarith.
+Hint Resolve Qeq_sym : qarith.
+Hint Resolve Qeq_trans : qarith.
 
 Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
 Proof.
@@ -633,8 +632,15 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
 Qed.
 
+(** These hints were meant to be added to the qarith database,
+    but a typo prevented that. This will be fixed in 8.3.
+    Concerning 8.2, for maximal compatibility , we
+    leave them in a separate database, in order to preserve
+    the strength of both [auto with qarith] and [auto with *].
+    (see bug #2346). *)
+
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
- Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
+ Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra.
 
 (** Some decidability results about orders. *)
 
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 71befa4a..34771897 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zbool.v 11208 2008-07-04 16:57:46Z letouzey $ *)
+(* $Id: Zbool.v 12271 2009-08-11 10:29:45Z herbelin $ *)
 
 Require Import BinInt.
 Require Import Zeven.
@@ -18,9 +18,9 @@ Require Import Sumbool.
 Unset Boxed Definitions.
 Open Local Scope Z_scope.
 
-(** * Boolean operations from decidabilty of order *)
+(** * Boolean operations from decidability of order *)
 (** The decidability of equality and order relations over
-    type [Z] give some boolean functions with the adequate specification. *)
+    type [Z] gives some boolean functions with the adequate specification. *)
 
 Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y).
 Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y).
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 425aa83b..73808f92 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
+(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*)
 
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
@@ -1025,3 +1025,5 @@ Qed.
 
 (** For compatibility *)
 Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
+Notation Zle_gt_succ := Zlt_gt_succ (only parsing).
+Notation Zle_succ_gt := Zlt_succ_gt (only parsing).