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. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90af20b4c..f2c74a3d0 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -123,7 +123,7 @@ ARGUMENT EXTEND auto_using' END module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ +module Vernac = Pvernac.Vernac_ module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located -- cgit v1.2.3