diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 07:17:57 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:57 -0400 |
| commit | f759aaf9de94a11aa34a31c869829d60243d273d (patch) | |
| tree | 3934cdf4dada8bd15be3b8f39bae36e6e3ad519b /vernac/proof_using.ml | |
| parent | ef3079e22fa7941d3335d7779c840e8d2d2bde39 (diff) | |
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Diffstat (limited to 'vernac/proof_using.ml')
| -rw-r--r-- | vernac/proof_using.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 8d0dcbf0fe..2130a398e9 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -169,7 +169,7 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us)) +let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) let proof_using_opt_name = ["Default";"Proof";"Using"] let () = |