aboutsummaryrefslogtreecommitdiff
path: root/coqpp
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-30 14:59:12 +0100
committerPierre-Marie Pédrot2018-11-30 14:59:12 +0100
commitae5cfac4f0c02f0cbd3f7286033a36c0e017538a (patch)
treefcc3d9bdaf3d6020bccc05e9de9a10d533c6648b /coqpp
parent2914348b9de1f86719a57b986f07041d8193f4eb (diff)
parent9703ac1003b7c64fec624f1e7d4407f84fdea873 (diff)
Merge PR #9064: [gramlib] Minor cleanups:
Diffstat (limited to 'coqpp')
-rw-r--r--coqpp/coqpp_main.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d52bd39d72..8d728b5b51 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -146,16 +146,16 @@ let print_local fmt ext =
fprintf fmt "in@ "
let print_position fmt pos = match pos with
-| First -> fprintf fmt "Extend.First"
-| Last -> fprintf fmt "Extend.Last"
-| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s
-| After s -> fprintf fmt "Extend.After@ \"%s\"" s
-| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s
+| First -> fprintf fmt "Gramlib.Gramext.First"
+| Last -> fprintf fmt "Gramlib.Gramext.Last"
+| Before s -> fprintf fmt "Gramlib.Gramext.Before@ \"%s\"" s
+| After s -> fprintf fmt "Gramlib.Gramext.After@ \"%s\"" s
+| Level s -> fprintf fmt "Gramlib.Gramext.Level@ \"%s\"" s
let print_assoc fmt = function
-| LeftA -> fprintf fmt "Extend.LeftA"
-| RightA -> fprintf fmt "Extend.RightA"
-| NonA -> fprintf fmt "Extend.NonA"
+| LeftA -> fprintf fmt "Gramlib.Gramext.LeftA"
+| RightA -> fprintf fmt "Gramlib.Gramext.RightA"
+| NonA -> fprintf fmt "Gramlib.Gramext.NonA"
let is_token s = match string_split s with
| [s] -> is_uident s