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: [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.
---
 tactics/class_tactics.ml | 4 ++--
 tactics/hints.ml         | 4 ++--
 tactics/hints.mli        | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b11e36bce..bbcf8def6 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 46d162911..739f1014a 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 1811150c2..b06ede0e1 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
-- 
cgit v1.2.3