diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 2e1bd6970..1ac597695 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()))) |