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. --- vernac/egramml.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/egramml.ml') diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 90cd7d10b..048d4d93a 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -77,7 +77,7 @@ let get_extend_vernac_rule (s, i) = | Failure _ -> raise Not_found let extend_vernac_command_grammar s nt gl = - let nt = Option.default Vernac_.command nt in + let nt = Option.default Pvernac.Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in -- cgit v1.2.3