aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/string_notation.ml')
-rw-r--r--plugins/syntax/string_notation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 8c0f9a3339..c92acb0f55 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope =
let of_ty = Smartlocate.global_with_alias g in
let cty = cref ty in
let arrow x y =
- mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+ mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
in
let constructors = get_constructors tyc in
(* Check the type of f *)