diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 16 | ||||
-rw-r--r-- | vernac/classes.mli | 6 | ||||
-rw-r--r-- | vernac/pvernac.mli | 2 | ||||
-rw-r--r-- | vernac/vernacexpr.ml | 10 |
4 files changed, 19 insertions, 15 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 40001c0a3..c82208980 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -50,11 +50,6 @@ let _ = let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) | IsGlobal gr -> Hints.IsGlobRef gr in - let info = - { info with hint_pattern = - Option.map - (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env()))) - info.hint_pattern } in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry @@ -63,10 +58,17 @@ let _ = Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) +let intern_info {hint_priority;hint_pattern} = + let env = Global.env() in + let sigma = Evd.from_env env in + let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in + {hint_priority;hint_pattern} + (** TODO: add subinstances *) let existing_instance glob g info = let c = global g in let info = Option.default Hints.empty_hint_info info in + let info = intern_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with @@ -107,6 +109,7 @@ open Pp let instance_hook k info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + let info = intern_info info in Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) @@ -301,7 +304,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if program_mode then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + let pri = intern_info pri in Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) in let obls, constr, typ = diff --git a/vernac/classes.mli b/vernac/classes.mli index 27d3a4669..631da8400 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 -> hint_info_expr option -> unit +val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : typeclass -> - hint_info_expr -> (** priority *) + Hints.hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) ?hook:(GlobRef.t -> unit) -> @@ -51,7 +51,7 @@ val new_instance : ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> - hint_info_expr -> + Hints.hint_info_expr -> Id.t (** Setting opacity *) diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 9d999793e..2993a1661 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -25,7 +25,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry - val hint_info : Typeclasses.hint_info_expr Gram.entry + val hint_info : Hints.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 291bd7a26..4ff9d105b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -119,11 +119,11 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = hint_pattern : 'a option } [@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] -type hint_info_expr = Typeclasses.hint_info_expr -[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] +type hint_info_expr = Hints.hint_info_expr +[@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] type hints_expr = Hints.hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -362,12 +362,12 @@ type nonrec vernac_expr = local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) - Typeclasses.hint_info_expr + Hints.hint_info_expr | VernacContext of local_binder_expr list | VernacDeclareInstances of - (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) + (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *) | VernacDeclareClass of reference (* inductive or definition name *) |