diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
| commit | af19d08003173718c0f7c070d0021ad958fbe58d (patch) | |
| tree | e148de88bbc70d6cd1561dffba2f301181bbb2f5 /vernac | |
| parent | 90ac335a32afc6bbca5c11b7be7aabc1f7abb89b (diff) | |
| parent | 81545ec98255e644be589d34a521924549e9e2fa (diff) | |
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 1 | ||||
| -rw-r--r-- | vernac/classes.mli | 6 |
2 files changed, 3 insertions, 4 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()))) diff --git a/vernac/classes.mli b/vernac/classes.mli index 0342c840e..e6134ee5d 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 *) |