aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-20 18:59:00 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-27 15:18:52 +0200
commit7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb (patch)
tree17940abdf158e6fd4ec435ba401678ed5f86d4ab /vernac/vernacentries.ml
parentb34acd7904dac581b57f7282192a40f1afb870dc (diff)
[api] Make `vernac/` self-contained.
We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7ca51db78..41c496a6b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1969,7 +1969,7 @@ let vernac_load interp fname =
interp x in
let parse_sentence = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Gram.entry_parse Pcoq.main_entry po with
+ match Pcoq.Gram.entry_parse Pvernac.main_entry po with
| Some x -> x
| None -> raise End_of_input) in
let fname =