diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 10 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 12 |
2 files changed, 13 insertions, 9 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 99d54755..9681d543 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*) +(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -479,8 +479,12 @@ Ltac intro_prototypes := | _ => idtac end. -Ltac do_case p := destruct p || elim_case p || (case p ; clear p). -Ltac do_ind p := induction p || elim_ind p. +Ltac introduce p := + first [ match p with _ => idtac end (* Already there *) + | intros until p | intros ]. + +Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)). +Ltac do_ind p := introduce p ; (induction p || elim_ind p). Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 12bdf3a7..2083e530 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *) +(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -165,7 +165,7 @@ Section Measure_well_founded. (* Measure relations are well-founded if the underlying relation is well-founded. *) - Variables T M: Set. + Variables T M: Type. Variable R: M -> M -> Prop. Hypothesis wf: well_founded R. Variable m: T -> M. @@ -191,7 +191,7 @@ End Measure_well_founded. Section Fix_measure_rects. - Variable A: Set. + Variable A: Type. Variable m: A -> nat. Variable P: A -> Type. Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x. @@ -287,7 +287,7 @@ Section Fix_measure_rects. End Fix_measure_rects. -(** Tactic to fold a definitions based on [Fix_measure_sub]. *) +(** Tactic to fold a definition based on [Fix_measure_sub]. *) Ltac fold_sub f := match goal with @@ -312,8 +312,8 @@ Module WfExtensionality. (** For a function defined with Program using a well-founded order. *) Program Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) + forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Type) (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = |