aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/numeral.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/numeral.ml')
-rw-r--r--plugins/syntax/numeral.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index a148a3bc73..9808c61255 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts =
let cty = mkRefC ty in
let app x y = mkAppC (x,[y]) 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 opt r = app (mkRefC (q_option ())) r in
let constructors = get_constructors tyc in