diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 12 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 4 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 14 |
4 files changed, 16 insertions, 16 deletions
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 69421255d..4d6d66c3d 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -18,7 +18,7 @@ Require Import Relation_Operators. Require Import Transitive_Closure. Section Wf_Lexicographic_Exponentiation. - Variable A : Set. + Variable A : Type. Variable leA : A -> A -> Prop. Notation Power := (Pow A leA). diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 82bede919..f41b6e93d 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -18,8 +18,8 @@ Require Import Transitive_Closure. L. Paulson JSC (1986) 2, 325-355 *) Section WfLexicographic_Product. - Variable A : Set. - Variable B : A -> Set. + Variable A : Type. + Variable B : A -> Type. Variable leA : A -> A -> Prop. Variable leB : forall x:A, B x -> B x -> Prop. @@ -74,8 +74,8 @@ End WfLexicographic_Product. Section Wf_Symmetric_Product. - Variable A : Set. - Variable B : Set. + Variable A : Type. + Variable B : Type. Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. @@ -106,7 +106,7 @@ End Wf_Symmetric_Product. Section Swap. - Variable A : Set. + Variable A : Type. Variable R : A -> A -> Prop. Notation SwapProd := (swapprod A R). @@ -168,4 +168,4 @@ Section Swap. apply Acc_swapprod; auto with sets. Qed. -End Swap.
\ No newline at end of file +End Swap. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 1866c5035..5e33da5ff 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -14,7 +14,7 @@ Require Import Relation_Definitions. Require Import Relation_Operators. Section Wf_Transitive_Closure. - Variable A : Set. + Variable A : Type. Variable R : relation A. Notation trans_clos := (clos_trans A R). @@ -44,4 +44,4 @@ Section Wf_Transitive_Closure. unfold well_founded in |- *; auto with sets. Qed. -End Wf_Transitive_Closure.
\ No newline at end of file +End Wf_Transitive_Closure. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index b1cb63be1..7296897ef 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -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. |