diff options
| author | Pierre-Marie Pédrot | 2018-11-22 11:40:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-23 13:59:15 +0100 |
| commit | bb4daa4af0515f3041203c5bcc0a1d8cd1123e5a (patch) | |
| tree | aa36956741fcc87ab5a69b086a983d005a0d1c9f | |
| parent | 6817d0da46adc07ad01b167d5362153d60e2f853 (diff) | |
Only use Coq API in coqpp.
| -rw-r--r-- | coqpp/coqpp_main.ml | 10 | ||||
| -rw-r--r-- | parsing/g_prim.mlg | 1 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mlg | 1 |
4 files changed, 5 insertions, 9 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 8da4c6db13..d52bd39d72 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -139,7 +139,7 @@ let print_local fmt ext = match locals with | [] -> () | e :: locals -> - let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in + let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in let () = List.iter iter locals in @@ -277,16 +277,16 @@ let print_rule fmt r = let pr_prd fmt prd = print_list fmt print_prod prd in fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) -let print_entry fmt gram e = +let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ " - gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ " + e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = let () = fprintf fmt "let _ = @[" in let () = fprintf fmt "@[<v>%a@]" print_local ext in - let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in + let () = List.iter (fun e -> print_entry fmt e) ext.gramext_entries in let () = fprintf fmt "()@]@\n" in () diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index dfb788907e..6247a12640 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -13,7 +13,6 @@ open Names open Libnames -open Pcoq open Pcoq.Prim let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2596bc22f2..f7375a0f01 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -226,8 +226,6 @@ let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer -open Pcoq - } GRAMMAR EXTEND Gram diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 3f0794fdd4..0dd17dfc15 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -11,7 +11,6 @@ { open Ltac_plugin -open Pcoq open Pcoq.Constr open Ssrmatching open Ssrmatching.Internal |