aboutsummaryrefslogtreecommitdiff
path: root/coqpp
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-24 20:22:23 +0100
committerEmilio Jesus Gallego Arias2018-11-27 15:12:03 +0100
commit1655407ac0525efa0fcd98ab85e3fd80a9f6cf64 (patch)
tree901f1b03ea71e5703b3feaf2c0d939fd35053ad3 /coqpp
parent39bf8df76fc1093f3efa672284421c884319c89d (diff)
[gramlib] Minor cleanups:
- remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter.
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