aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6b8fcdead..976677f8c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -220,8 +220,8 @@ type vernac_expr =
export_flag option * specif_flag option * lreference list
| VernacImport of export_flag * lreference list
| VernacCanonical of lreference
- | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr
- | VernacIdentityCoercion of strength * lident *
+ | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr
+ | VernacIdentityCoercion of locality * lident *
class_rawexpr * class_rawexpr
(* Type classes *)