From b34acd7904dac581b57f7282192a40f1afb870dc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 00:15:44 +0200
Subject: [tactics] Turn boolean locality hint parameter into a named one.

---
 plugins/ltac/extratactics.ml4 | 2 +-
 plugins/ltac/g_auto.ml4       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23f..757451882e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r =
 
 let add_hints_iff ~atts l2r lc n bl =
   let open Vernacinterp in
-  Hints.add_hints (Locality.make_module_locality atts.locality) bl
+  Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
     (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
 
 VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99f7..07047d0162 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
     fun ~atts ~st -> begin
         let open Vernacinterp in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        Hints.add_hints (Locality.make_section_locality atts.locality)
+        Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
         st
       end
-- 
cgit v1.2.3


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/ltac/g_ltac.ml4    | 8 ++++----
 plugins/ltac/g_rewrite.ml4 | 2 +-
 plugins/ltac/g_tactic.ml4  | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 4857beffa8..ed54320a59 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -21,9 +21,9 @@ open Tok (* necessary for camlp5 *)
 open Names
 
 open Pcoq
-open Pcoq.Constr
-open Pcoq.Vernac_
 open Pcoq.Prim
+open Pcoq.Constr
+open Pvernac.Vernac_
 open Pltac
 
 let fail_default_value = ArgArg 0
@@ -58,8 +58,8 @@ let tacdef_body = new_entry "tactic:tacdef_body"
 let _ =
   let mode = {
     Proof_global.name = "Classic";
-    set = (fun () -> set_command_entry tactic_mode);
-    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+    set = (fun () -> Pvernac.set_command_entry tactic_mode);
+    reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
   } in
   Proof_global.register_proof_mode mode
 
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fbaa2e58f7..079001ee40 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -20,9 +20,9 @@ open Extraargs
 open Tacmach
 open Rewrite
 open Stdarg
-open Pcoq.Vernac_
 open Pcoq.Prim
 open Pcoq.Constr
+open Pvernac.Vernac_
 open Pltac
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 7534e27999..dc9f607cf0 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -211,7 +211,7 @@ let warn_deprecated_eqn_syntax =
 
 (* Auxiliary grammar rules *)
 
-open Vernac_
+open Pvernac.Vernac_
 
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-- 
cgit v1.2.3