aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-02-07 14:42:26 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-02-07 14:42:26 +0000
commit6b006ec56f9750293c5ac6c8f69233d37318f41d (patch)
treec860a753439b5432de12a3873d5e62ea0adb2e4d /theories
parent7bc476283db30b0d611e78962050de65bd061e68 (diff)
Backtrack sur le passage de Set à Type pour l'ordre lexicographique
pour garder Relation_Operators.Pow dans Set (puisque le polymorphisme d'univers pour les inductifs ne se propage pas aux définitions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Relations/Relation_Operators.v4
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v2
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index c8ace84c3..8d76b4f4e 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -138,7 +138,7 @@ End Swap.
Section Lexicographic_Exponentiation.
- Variable A : Type.
+ Variable A : Set.
Variable leA : A -> A -> Prop.
Let Nil := nil (A:=A).
Let List := list A.
@@ -156,7 +156,7 @@ Section Lexicographic_Exponentiation.
forall (x y:A) (l:List),
leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
- Definition Pow : Type := sig Desc.
+ Definition Pow : Set := sig Desc.
Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 4d6d66c3d..69421255d 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 : Type.
+ Variable A : Set.
Variable leA : A -> A -> Prop.
Notation Power := (Pow A leA).