diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 14 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 6 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 16 |
4 files changed, 19 insertions, 19 deletions
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 24816a20..efdf0495 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lexicographic_Exponentiation.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Lexicographic_Exponentiation.v 9610 2007-02-07 14:45:18Z herbelin $ i*) (** Author: Cristina Cornes diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 8ac0d546..051c8127 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lexicographic_Product.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Lexicographic_Product.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** Authors: Bruno Barras, Cristina Cornes *) @@ -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 5bf82ffb..bd4e4fec 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Transitive_Closure.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Transitive_Closure.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** Author: Bruno Barras *) @@ -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 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. |