aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/IntMap/Map.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/IntMap/Map.v')
-rw-r--r--theories/IntMap/Map.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index 6b914264f..96c89691d 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -25,9 +25,9 @@ Definition ad := N.
Section MapDefs.
(** We now define maps from ad to A. *)
- Variable A : Set.
+ Variable A : Type.
- Inductive Map : Set :=
+ Inductive Map :=
| M0 : Map
| M1 : ad -> A -> Map
| M2 : Map -> Map -> Map.