aboutsummaryrefslogtreecommitdiffstats
path: root/common/Unityping.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Unityping.v')
-rw-r--r--common/Unityping.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Unityping.v b/common/Unityping.v
index f9c9d72c..28bcfb5c 100644
--- a/common/Unityping.v
+++ b/common/Unityping.v
@@ -28,9 +28,9 @@ Local Open Scope error_monad_scope.
Module Type TYPE_ALGEBRA.
-Variable t: Type.
-Variable eq: forall (x y: t), {x=y} + {x<>y}.
-Variable default: t.
+Parameter t: Type.
+Parameter eq: forall (x y: t), {x=y} + {x<>y}.
+Parameter default: t.
End TYPE_ALGEBRA.