From 81545ec98255e644be589d34a521924549e9e2fa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 24 Apr 2018 18:46:18 +0200
Subject: [PATCH] [api] Move `hint_info_expr` to `Typeclasses`.

`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
---
 parsing/g_vernac.ml4          |  6 +++---
 parsing/pcoq.mli              |  2 +-
 plugins/ltac/extratactics.ml4 |  2 +-
 pretyping/typeclasses.ml      | 15 ++++++++++-----
 pretyping/typeclasses.mli     | 22 ++++++++++++++--------
 pretyping/vernacexpr.ml       | 12 +++++++-----
 printing/ppvernac.ml          |  2 +-
 tactics/class_tactics.ml      |  4 ++--
 tactics/hints.ml              |  4 ++--
 tactics/hints.mli             |  4 ++--
 vernac/classes.ml             |  1 -
 vernac/classes.mli            |  6 +++---
 12 files changed, 46 insertions(+), 34 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2dbd624c2caa..b3bc895ba6cc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -645,7 +645,7 @@ GEXTEND Gram
 
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
         pri = OPT [ "|"; i = natural -> i ] ->
-         let info = { hint_priority = pri; hint_pattern = None } in
+         let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
          let insts = List.map (fun i -> (i, info)) ids in
 	  VernacDeclareInstances insts
 
@@ -770,8 +770,8 @@ GEXTEND Gram
   ;
   hint_info:
     [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
-         { hint_priority = i; hint_pattern = pat }
-      | -> { hint_priority = None; hint_pattern = None } ] ]
+         { Typeclasses.hint_priority = i; hint_pattern = pat }
+      | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ]
   ;
   reserv_list:
     [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9f186224b9c2..0fbf2f567f2e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -260,7 +260,7 @@ module Vernac_ :
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
-    val hint_info : Vernacexpr.hint_info_expr Gram.entry
+    val hint_info : Typeclasses.hint_info_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a5f8060aee45..797dfbe23f77 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint ~poly pri l2r r =
   let ctx = Evd.const_univ_entry ~poly sigma in
   let c = EConstr.to_constr sigma c in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-  let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
+  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff ~atts l2r lc n bl =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 30ddeffa6904..e73a78fb84be 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 (*i*)
 
+(* Core typeclasses hints *)
+type 'a hint_info_gen =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
 let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
@@ -73,7 +80,7 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+  cl_projs : (Name.t * (direction * hint_info_expr) option
 	      * Constant.t option) list;
   
   cl_strict : bool;
@@ -85,7 +92,7 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: global_reference;
-  is_info: Vernacexpr.hint_info_expr;
+  is_info: hint_info_expr;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
@@ -96,7 +103,7 @@ type instances = (instance Refmap.t) Refmap.t
 
 let instance_impl is = is.is_impl
 
-let hint_priority is = is.is_info.Vernacexpr.hint_priority
+let hint_priority is = is.is_info.hint_priority
 
 let new_instance cl info glob impl =
   let global =
@@ -266,8 +273,6 @@ let check_instance env sigma c =
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
-open Vernacexpr
-
 let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
   let _next_id = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b80c287117c9..e50d90b1563f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,13 @@ open Environ
 
 type direction = Forward | Backward
 
+(* Core typeclasses hints *)
+type 'a hint_info_gen =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 (** This module defines type-classes *)
 type typeclass = {
   (** The toplevel universe quantification in which the typeclass lives. In
@@ -37,7 +44,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list;
+  cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -55,8 +62,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
-  global_reference -> instance
+val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
 
@@ -123,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook : 
   (global_reference_or_constr -> global_reference list ->
-   bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
-  bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
+  bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
+val declare_instance : hint_info_expr option -> bool -> global_reference -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
@@ -140,5 +146,5 @@ val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_refere
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
-		       Vernacexpr.hint_info_expr ->
-		       (global_reference list * Vernacexpr.hint_info_expr * constr) list
+                       hint_info_expr ->
+                       (global_reference list * hint_info_expr * constr) list
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 4e1c986f16e0..f0e5f5746f56 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -115,14 +115,16 @@ type hint_mode =
   | ModeNoHeadEvar (* No evar at the head *)
   | ModeOutput (* Anything *)
 
-type 'a hint_info_gen =
+type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
+[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"]
 
-type hint_info_expr = constr_pattern_expr hint_info_gen
+type hint_info_expr = Typeclasses.hint_info_expr
+[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
 
 type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | 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
@@ -362,12 +364,12 @@ type nonrec vernac_expr =
       local_binder_expr list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(bool * constr_expr) option * (* props *)
-	hint_info_expr
+        Typeclasses.hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
-    (reference * hint_info_expr) list (* instances names, priorities and patterns *)
+    (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 83c875707007..6ad8572339c1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -188,7 +188,7 @@ open Pputils
     | ModeNoHeadEvar -> str"!"
     | ModeOutput -> str"-"
 
-  let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+  let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
     pr_opt (fun x -> str"|" ++ int x) pri ++
     pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b11e36bceb94..bbcf8def6de6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
 	      let info =
-		{ info with Vernacexpr.hint_pattern =
+                { info with hint_pattern =
                             Option.map (Constrintern.intern_constr_pattern env sigma)
-				       info.Vernacexpr.hint_pattern }
+                                       info.hint_pattern }
 	      in
 	      make_resolves env sigma ~name:(PathHints path)
                   (true,false,not !Flags.quiet) info false
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 46d16291194d..739f1014a71a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,12 +28,13 @@ open Termops
 open Inductiveops
 open Typing
 open Decl_kinds
+open Vernacexpr
+open Typeclasses
 open Pattern
 open Patternops
 open Clenv
 open Tacred
 open Printer
-open Vernacexpr
 
 module NamedDecl = Context.Named.Declaration
 
@@ -94,7 +95,6 @@ let secvars_of_hyps hyps =
   else pred
 
 let empty_hint_info =
-  let open Vernacexpr in
   { hint_priority = None; hint_pattern = None }
 
 (************************************************************************)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c2a21..b06ede0e1626 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -31,7 +31,7 @@ type debug = Debug | Info | Off
 
 val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
 
-val empty_hint_info : 'a hint_info_gen
+val empty_hint_info : 'a Typeclasses.hint_info_gen
 
 (** Pre-created hint databases *)
 
@@ -144,7 +144,7 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
 
 type hint_term =
   | IsGlobRef of global_reference
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 7f2642093fe4..906b4a959c0e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -51,7 +51,6 @@ let _ =
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
      let info =
-       let open Vernacexpr in
        { info with hint_pattern =
 		   Option.map
                      (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 0342c840ee31..e6134ee5dd59 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,12 +22,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+val existing_instance : bool -> reference -> hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  Vernacexpr.hint_info_expr -> (** priority *)
+  hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
@@ -51,7 +51,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
-  Vernacexpr.hint_info_expr ->
+  hint_info_expr ->
   Id.t
 
 (** Setting opacity *)