diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Tactics.v | 6 | ||||
| -rw-r--r-- | theories/Init/Wf.v | 19 |
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. |