aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/IntMap/Mapcanon.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/IntMap/Mapcanon.v')
-rw-r--r--theories/IntMap/Mapcanon.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index 0b922864f..794ecb12c 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -24,7 +24,7 @@ Require Import Mapcard.
Section MapCanon.
- Variable A : Set.
+ Variable A : Type.
Inductive mapcanon : Map A -> Prop :=
| M0_canon : mapcanon (M0 A)
@@ -277,7 +277,7 @@ Section MapCanon.
exact (mapcanon_M2_2 _ _ H4).
Qed.
- Variable B : Set.
+ Variable B : Type.
Lemma MapDomRestrTo_canon :
forall m:Map A,
@@ -337,7 +337,7 @@ End MapCanon.
Section FSetCanon.
- Variable A : Set.
+ Variable A : Type.
Lemma MapDom_canon :
forall m:Map A, mapcanon A m -> mapcanon unit (MapDom A m).
@@ -354,7 +354,7 @@ End FSetCanon.
Section MapFoldCanon.
- Variables A B : Set.
+ Variables A B : Type.
Lemma MapFold_canon_1 :
forall m0:Map B,