summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /theories/Init
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Tactics.v6
-rw-r--r--theories/Init/Wf.v19
2 files changed, 5 insertions, 20 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index afe8297e..10555fc0 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 11072 2008-06-08 16:13:37Z herbelin $ i*)
+(*i $Id: Tactics.v 11309 2008-08-06 10:30:35Z herbelin $ i*)
Require Import Notations.
Require Import Logic.
@@ -115,7 +115,7 @@ lazymatch T with
evar (a : t); pose proof (H a) as H1; unfold a in H1;
clear a; clear H; rename H1 into H; find_equiv H
| ?A <-> ?B => idtac
-| _ => fail "The given statement does not seem to end with an equivalence"
+| _ => fail "The given statement does not seem to end with an equivalence."
end.
Ltac bapply lemma todo :=
@@ -141,7 +141,7 @@ t;
match goal with
| H : _ |- _ => solve [inversion H]
| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
-| _ => fail 1 "Cannot solve this goal"
+| _ => fail 1 "Cannot solve this goal."
end.
(** A tactic to document or check what is proved at some point of a script *)
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index f46b2b11..d3f8f1ab 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf.v 10712 2008-03-23 11:38:38Z herbelin $ i*)
+(*i $Id: Wf.v 11251 2008-07-24 08:28:40Z herbelin $ i*)
(** * This module proves the validity of
- well-founded recursion (also known as course of values)
@@ -27,6 +27,7 @@ Section Well_founded.
Variable R : A -> A -> Prop.
(** The accessibility predicate is defined to be non-informative *)
+ (** (Acc_rect is automatically defined because Acc is a singleton type) *)
Inductive Acc (x: A) : Prop :=
Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
@@ -35,22 +36,6 @@ Section Well_founded.
destruct 1; trivial.
Defined.
- (** Informative elimination :
- [let Acc_rec F = let rec wf x = F x wf in wf] *)
-
- Section AccRecType.
-
- Variable P : A -> Type.
- Variable F : forall x:A,
- (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
-
- Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
- F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)).
-
- End AccRecType.
-
- Definition Acc_rec (P:A -> Set) := Acc_rect P.
-
(** A relation is well-founded if every element is accessible *)
Definition well_founded := forall a:A, Acc a.