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.

---
 tactics/hints.ml  | 2 +-
 tactics/hints.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ade5314b9..17e9775b07 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1322,7 +1322,7 @@ let interp_hints poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c7de10a2a5..7ec70e72e0 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -178,7 +178,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : polymorphic -> hints_expr -> hints_entry
 
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
-- 
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.
---
 tactics/hints.ml  | 19 ++++++++++++++++++-
 tactics/hints.mli | 19 ++++++++++++++++++-
 2 files changed, 36 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 17e9775b07..8755658d50 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,7 +28,6 @@ open Termops
 open Inductiveops
 open Typing
 open Decl_kinds
-open Vernacexpr
 open Typeclasses
 open Pattern
 open Patternops
@@ -156,6 +155,24 @@ type full_hint = hint with_metadata
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
+type reference_or_constr =
+  | HintsReference of reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
+  | HintsMode of reference * hint_mode list
+  | HintsConstructors of reference list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type import_level = [ `LAX | `WARN | `STRICT ]
 
 let warn_hint : import_level ref = ref `LAX
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 7ec70e72e0..f059887031 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -18,7 +18,6 @@ open Misctypes
 open Tactypes
 open Clenv
 open Pattern
-open Vernacexpr
 
 (** {6 General functions. } *)
 
@@ -71,6 +70,24 @@ type search_entry
 
 type hint_entry
 
+type reference_or_constr =
+  | HintsReference of Libnames.reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.reference list
+  | HintsTransparency of Libnames.reference list * bool
+  | HintsMode of Libnames.reference * hint_mode list
+  | HintsConstructors of Libnames.reference list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
   | PathStar of 'a hints_path_gen
-- 
cgit v1.2.3