From 8b302bfba8f98458087685c8d5fbca2cf647255f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 21 May 2018 10:45:28 +0200
Subject: Move interning the [hint_pattern] outside the Typeclasses hooks.

Close #7562.

[api] move hint_info ast to tactics.
---
 pretyping/typeclasses.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 12a944d322..70588b6ad0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
 
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
@@ -80,7 +80,7 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * hint_info_expr) option
+  cl_projs : (Name.t * (direction * hint_info) option
 	      * Constant.t option) list;
   
   cl_strict : bool;
@@ -92,7 +92,7 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: GlobRef.t;
-  is_info: hint_info_expr;
+  is_info: hint_info;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
-- 
cgit v1.2.3