From 7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 20 May 2018 18:59:00 +0200 Subject: [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. --- dev/base_include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/base_include') diff --git a/dev/base_include b/dev/base_include index 2f5d8aa84..87913cfbe 100644 --- a/dev/base_include +++ b/dev/base_include @@ -189,7 +189,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; +let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;; let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of -- cgit v1.2.3