diff options
Diffstat (limited to 'theories/Wellfounded/Well_Ordering.v')
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 69617de2..f691f2b7 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Well_Ordering.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Well_Ordering.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory @@ -15,10 +15,10 @@ Require Import Eqdep. Section WellOrdering. - Variable A : Set. - Variable B : A -> Set. + Variable A : Type. + Variable B : A -> Type. - Inductive WO : Set := + Inductive WO : Type := sup : forall (a:A) (f:B a -> WO), WO. @@ -52,7 +52,7 @@ Section Characterisation_wf_relations. (* in course of development *) - Variable A : Set. + Variable A : Type. Variable leA : A -> A -> Prop. Definition B (a:A) := {x : A | leA x a}. @@ -60,12 +60,12 @@ Section Characterisation_wf_relations. Definition wof : well_founded leA -> A -> WO A B. Proof. intros. - apply (well_founded_induction H (fun a:A => WO A B)); auto. - intros. + apply (well_founded_induction_type H (fun a:A => WO A B)); auto. + intros x H1. apply (sup A B x). unfold B at 1 in |- *. destruct 1 as [x0]. apply (H1 x0); auto. Qed. -End Characterisation_wf_relations.
\ No newline at end of file +End Characterisation_wf_relations. |