summaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FSetDecide.v20
-rw-r--r--theories/Init/Notations.v10
-rw-r--r--theories/Init/Tactics.v19
-rw-r--r--theories/Lists/List.v8
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v7
-rw-r--r--theories/QArith/QArith_base.v28
-rw-r--r--theories/ZArith/Zbool.v6
-rw-r--r--theories/ZArith/Zorder.v4
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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 20:56:16 +0000