From 81545ec98255e644be589d34a521924549e9e2fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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. --- vernac/classes.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 7f2642093..906b4a959 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()))) -- cgit v1.2.3