aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/Classes.tex2
-rw-r--r--doc/refman/RefMan-tac.tex6
-rw-r--r--intf/vernacexpr.mli12
-rw-r--r--ltac/extratactics.ml43
-rw-r--r--ltac/rewrite.ml8
-rw-r--r--parsing/g_proofs.ml410
-rw-r--r--parsing/g_vernac.ml426
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--pretyping/typeclasses.ml48
-rw-r--r--pretyping/typeclasses.mli17
-rw-r--r--printing/ppvernac.ml22
-rw-r--r--printing/prettyp.ml2
-rw-r--r--tactics/class_tactics.ml18
-rw-r--r--tactics/hints.ml87
-rw-r--r--tactics/hints.mli36
-rw-r--r--test-suite/success/Hints.v6
-rw-r--r--toplevel/classes.ml33
-rw-r--r--toplevel/classes.mli8
-rw-r--r--toplevel/record.ml5
-rw-r--r--toplevel/record.mli3
-rw-r--r--toplevel/vernacentries.ml10
22 files changed, 212 insertions, 152 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 144fc22b9..254fca28f 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -379,7 +379,7 @@ Declares variables according to the given binding context, which might
use implicit generalization (see \ref{SectionContext}).
\asubsection{\tt typeclasses eauto}
-\tacindex{typeclasseseauto}
+\tacindex{typeclasses eauto}
The {\tt typeclasses eauto} tactic uses a different resolution engine
than {\tt eauto} and {\tt auto}. The main differences are the following:
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c659e19e6..0aa179d62 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3718,12 +3718,14 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is
The {\hintdef} is one of the following expressions:
\begin{itemize}
-\item {\tt Resolve \term}
+\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}}
\comindex{Hint Resolve}
This command adds {\tt simple apply {\term}} to the hint list
with the head symbol of the type of \term. The cost of that hint is
- the number of subgoals generated by {\tt simple apply {\term}}.
+ the number of subgoals generated by {\tt simple apply {\term}} or \num
+ if specified. The associated pattern is inferred from the conclusion
+ of the type of \term or the given \pattern if specified.
%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
In case the inferred type of \term\ does not start with a product
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 1336c92b6..92e4dd618 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -123,8 +123,14 @@ type hint_mode =
| ModeNoHeadEvar (* No evar at the head *)
| ModeOutput (* Anything *)
+type 'a hint_info_gen =
+ { hint_priority : int option;
+ hint_pattern : 'a option }
+
+type hint_info_expr = constr_pattern_expr hint_info_gen
+
type hints_expr =
- | HintsResolve of (int option * bool * reference_or_constr) list
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
| HintsImmediate of reference_or_constr list
| HintsUnfold of reference list
| HintsTransparency of reference list * bool
@@ -368,12 +374,12 @@ type vernac_expr =
local_binder list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
(bool * constr_expr) option * (* props *)
- int option (* Priority *)
+ hint_info_expr
| VernacContext of local_binder list
| VernacDeclareInstances of
- reference list * int option (* instance names, priority *)
+ (reference * hint_info_expr) list (* instances names, priorities and patterns *)
| VernacDeclareClass of reference (* inductive or definition name *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d0318fb5f..063bfbe6d 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -316,7 +316,8 @@ let project_hint pri l2r r =
in
let ctx = Evd.universe_context_set sigma in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
- (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
+ let info = Vernacexpr.({hint_priority = pri; hint_pattern = None}) in
+ (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
let add_hints_iff l2r lc n bl =
Hints.add_hints true bl
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 4d7c5d0e4..44efdd383 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1788,7 +1788,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
binders instance (Some (true, CRecord (Loc.ghost,fields)))
- ~global ~generalize:false ~refine:false None
+ ~global ~generalize:false ~refine:false Hints.empty_hint_info
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -1969,7 +1969,7 @@ let add_morphism_infer glob m n =
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) None glob
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
poly (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
else
@@ -1980,7 +1980,7 @@ let add_morphism_infer glob m n =
let hook _ = function
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) None
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
glob poly (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
@@ -2004,7 +2004,7 @@ let add_morphism glob binders m s n =
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~global:glob poly binders instance
(Some (true, CRecord (Loc.ghost,[])))
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e3c4b880..70c5d5d88 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -103,10 +103,9 @@ GEXTEND Gram
(* Declare "Resolve" explicitly so as to be able to later extend with
"Resolve ->" and "Resolve <-" *)
| IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr;
- pri = OPT [ "|"; i = natural -> i ];
- dbnames = opt_hintbases ->
+ info = hint_info; dbnames = opt_hintbases ->
VernacHints (false,dbnames,
- HintsResolve (List.map (fun x -> (pri, true, x)) lc))
+ HintsResolve (List.map (fun x -> (info, true, x)) lc))
] ];
obsolete_locality:
[ [ IDENT "Local" -> true | -> false ] ]
@@ -116,9 +115,8 @@ GEXTEND Gram
| c = constr -> HintsConstr c ] ]
;
hint:
- [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr;
- pri = OPT [ "|"; i = natural -> i ] ->
- HintsResolve (List.map (fun x -> (pri, true, x)) lc)
+ [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
+ HintsResolve (List.map (fun x -> (info, true, x)) lc)
| IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
| IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
| IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e0d836df8..ffc27d605 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,7 +582,7 @@ let warn_deprecated_implicit_arguments =
(* Extensions: implicits, coercions, etc. *)
GEXTEND Gram
- GLOBAL: gallina_ext instance_name;
+ GLOBAL: gallina_ext instance_name hint_info;
gallina_ext:
[ [ (* Transparent and Opaque *)
@@ -635,17 +635,20 @@ GEXTEND Gram
| IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ;
+ info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) |
":="; c = lconstr -> Some (false,c) | -> None ] ->
- VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri)
+ VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info)
| IDENT "Existing"; IDENT "Instance"; id = global;
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacDeclareInstances ([id], pri)
+ info = hint_info ->
+ VernacDeclareInstances [id, info]
+
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacDeclareInstances (ids, pri)
+ pri = OPT [ "|"; i = natural -> i ] ->
+ let info = { hint_priority = pri; hint_pattern = None } in
+ let insts = List.map (fun i -> (i, info)) ids in
+ VernacDeclareInstances insts
| IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
@@ -786,6 +789,11 @@ GEXTEND Gram
(Option.default [] sup)
| -> ((!@loc, Anonymous), None), [] ] ]
;
+ hint_info:
+ [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
+ { hint_priority = i; hint_pattern = pat }
+ | -> { hint_priority = None; hint_pattern = None } ] ]
+ ;
reserv_list:
[ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
;
@@ -807,8 +815,8 @@ GEXTEND Gram
(* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
| IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
- pri = OPT [ "|"; i = natural -> i ] ->
- VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri)
+ info = hint_info ->
+ VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info)
(* System directory *)
| IDENT "Pwd" -> VernacChdir None
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 9e9a7e723..7dc02190e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -379,6 +379,7 @@ module Vernac_ =
let vernac = gec_vernac "Vernac.vernac"
let vernac_eoi = eoi_entry vernac
let rec_definition = gec_vernac "Vernac.rec_definition"
+ let hint_info = gec_vernac "hint_info"
(* Main vernac entry *)
let main_entry = Gram.entry_create "vernac"
let noedit_mode = gec_vernac "noedit_command"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7f6caf63f..ec8dac821 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,6 +213,7 @@ module Vernac_ :
val vernac_eoi : vernac_expr Gram.entry
val noedit_mode : vernac_expr Gram.entry
val command_entry : vernac_expr Gram.entry
+ val hint_info : Vernacexpr.hint_info_expr Gram.entry
end
(** The main entry: reads an optional vernac command *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 31ef3dfdd..b8da6b685 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,8 @@ type typeclass = {
cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
- cl_projs : (Name.t * (direction * int option) option * constant option) list;
+ cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+ * constant option) list;
cl_strict : bool;
@@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t
type instance = {
is_class: global_reference;
- is_pri: int option;
+ is_info: Vernacexpr.hint_info_expr;
(* Sections where the instance should be redeclared,
- -1 for discard, 0 for none, mutable to avoid redeclarations
- when multiple rebuild_object happen. *)
+ -1 for discard, 0 for none. *)
is_global: int;
is_poly: bool;
is_impl: global_reference;
@@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t
let instance_impl is = is.is_impl
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
let global =
if glob then Lib.sections_depth ()
else -1
in
{ is_class = cl.cl_impl;
- is_pri = pri ;
+ is_info = info ;
is_global = global ;
is_poly = poly;
is_impl = impl }
@@ -274,7 +274,9 @@ let check_instance env sigma c =
not (Evd.has_undefined evd)
with e when CErrors.noncritical e -> false
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
let _id = Nametab.basename_of_global glob in
let _next_id =
let i = ref (-1) in
@@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri =
match b with
| None -> None
| Some (Backward, _) -> None
- | Some (Forward, pri') ->
+ | Some (Forward, info) ->
let proj = Option.get proj in
let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
if check && check_instance env sigma body then None
else
- let pri =
- match pri, pri' with
+ let newpri =
+ match pri, info.hint_priority with
| Some p, Some p' -> Some (p + p')
| Some p, None -> Some (p + 1)
| _, _ -> None
in
- Some (ConstRef proj, pri, body)) tc.cl_projs
+ Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
in
- let declare_proj hints (cref, pri, body) =
+ let declare_proj hints (cref, info, body) =
let path' = cref :: path in
let ty = Retyping.get_type_of env sigma body in
let rest = aux pri body ty path' in
- hints @ (path', pri, body) :: rest
+ hints @ (path', info, body) :: rest
in List.fold_left declare_proj [] projs
in
let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
let poly = Global.is_polymorphic inst.is_impl in
add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst)
- inst.is_pri poly;
+ inst.is_info poly;
List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
(is_local inst) pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
- (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+ (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
let rebuild_instance (action, inst) =
let () = match action with
@@ -404,26 +406,22 @@ let remove_instance i =
Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
remove_instance_hint i.is_impl
-let declare_instance pri local glob =
+let declare_instance info local glob =
let ty = Global.type_of_global_unsafe glob in
+ let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr ty with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* Auto.add_hints local [typeclasses_db] *)
-(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+ add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
| None -> ()
let add_class cl =
add_class cl;
List.iter (fun (n, inst, body) ->
match inst with
- | Some (Backward, pri) ->
+ | Some (Backward, info) ->
(match body with
| None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
- | Some b -> declare_instance pri false (ConstRef b))
+ | Some b -> declare_instance (Some info) false (ConstRef b))
| _ -> ())
cl.cl_projs
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2530f5dfa..620bc367b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,7 +32,7 @@ type typeclass = {
Some may be undefinable due to sorting restrictions or simply undefined if
no name is provided. The [int option option] indicates subclasses whose hint has
the given priority. *)
- cl_projs : (Name.t * (direction * int option) option * constant option) list;
+ cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
(** Whether we use matching or full unification during resolution *)
cl_strict : bool;
@@ -50,7 +50,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
global_reference -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
@@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr
val instance_impl : instance -> global_reference
-val instance_priority : instance -> int option
+val hint_priority : instance -> int option
val is_class : global_reference -> bool
val is_instance : global_reference -> bool
@@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state
val add_instance_hint_hook :
(global_reference_or_constr -> global_reference list ->
- bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t
+ bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (global_reference -> unit) Hook.t
val add_instance_hint : global_reference_or_constr -> global_reference list ->
- bool -> int option -> Decl_kinds.polymorphic -> unit
+ bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : global_reference -> unit
val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t
-val declare_instance : int option -> bool -> global_reference -> unit
+val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
(** Build the subinstances hints for a given typeclass object.
check tells if we should check for existence of the
subinstances and add only the missing ones. *)
-val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
- (global_reference list * int option * constr) list
+val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+ Vernacexpr.hint_info_expr ->
+ (global_reference list * Vernacexpr.hint_info_expr * constr) list
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5455ab891..3494ad006 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -166,14 +166,17 @@ module Make
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
+ let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+ pr_opt (fun x -> str"|" ++ int x) pri ++
+ pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
- (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++
- match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+ (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
l
| HintsImmediate l ->
keyword "Immediate" ++ spc() ++
@@ -888,7 +891,7 @@ module Make
spc() ++ pr_class_rawexpr c2)
)
- | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
return (
hov 1 (
(if abst then keyword "Declare" ++ spc () else mt ()) ++
@@ -899,7 +902,7 @@ module Make
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_priority pri ++
+ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
(match props with
| Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
| Some (true,_) -> assert false
@@ -913,11 +916,14 @@ module Make
keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
)
- | VernacDeclareInstances (ids, pri) ->
- return (
+ | VernacDeclareInstances insts ->
+ let pr_inst (id, info) =
+ pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+ in
+ return (
hov 1 (keyword "Existing" ++ spc () ++
- keyword(String.plural (List.length ids) "Instance") ++
- spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
+ keyword(String.plural (List.length insts) "Instance") ++
+ spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
)
| VernacDeclareClass id ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b590a8c93..e117f1dcb 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -872,7 +872,7 @@ let pr_instance env i =
(* gallina_print_constant_with_infos i.is_impl *)
(* lighter *)
print_ref false (instance_impl i) ++
- begin match instance_priority i with
+ begin match hint_priority i with
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
end
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9cb6b7fe7..da91674f5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -539,10 +539,16 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let name = PathHints [VarRef id] in
let hints =
if is_class then
- let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+ let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
(List.map_append
- (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
- (true,false,Flags.is_verbose()) pri false
+ (fun (path,info,c) ->
+ let info =
+ { info with Vernacexpr.hint_pattern =
+ Option.map (Constrintern.intern_constr_pattern env)
+ info.Vernacexpr.hint_pattern }
+ in
+ make_resolves env sigma ~name:(PathHints path)
+ (true,false,Flags.is_verbose()) info false
(IsConstr (c,Univ.ContextSet.empty)))
hints)
else []
@@ -567,7 +573,7 @@ let make_hints g st only_classes sign =
in
if consider then
let hint =
- pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+ pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
in hint @ hints
else hints)
([]) sign
@@ -636,7 +642,7 @@ module V85 = struct
let env = Goal.V82.env s g' in
let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
- (true,false,false) info.only_classes None (List.hd context) in
+ (true,false,false) info.only_classes empty_hint_info (List.hd context) in
let ldb = Hint_db.add_list env s hint info.hints in
(g', { info with is_evar = None; hints = ldb;
auto_last_tac = lazy (str"intro") })) gls
@@ -1140,7 +1146,7 @@ module Search = struct
let decl = Tacmach.New.pf_last_hyp gl in
let hint =
make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
- (true,false,false) info.search_only_classes None decl in
+ (true,false,false) info.search_only_classes empty_hint_info decl in
let ldb = Hint_db.add_list env s hint info.search_hints in
let info' =
{ info with search_hints = ldb; last_tac = lazy (str"intro") }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 823af0b0a..9cbfe20d9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -84,6 +84,8 @@ let secvars_of_hyps hyps =
if all then Id.Pred.full (* If the whole section context is available *)
else pred
+let empty_hint_info = Vernacexpr.{ hint_priority = None; hint_pattern = None }
+
(************************************************************************)
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
@@ -736,7 +738,7 @@ let secvars_of_constr env c =
let secvars_of_global env gr =
secvars_of_idset (vars_of_global_reference env gr)
-let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
let secvars = secvars_of_constr env c in
let cty = strip_outer_cast cty in
match kind_of_term cty with
@@ -747,16 +749,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
in
- (Some hd,
- { pri = (match pri with None -> 0 | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- db = None;
- secvars;
- code = with_uid (Give_exact (c, cty, ctx)); })
+ let pri = match info.hint_priority with None -> 0 | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some pat -> snd pat
+ | None -> pat
+ in
+ (Some hd,
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
+ code = with_uid (Give_exact (c, cty, ctx)); })
-let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
match kind_of_term cty with
| Prod _ ->
@@ -769,12 +772,13 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
with BoundPattern -> failwith "make_apply_entry" in
let nmiss = List.length (clenv_missing ce) in
let secvars = secvars_of_constr env c in
+ let pri = match info.hint_priority with None -> nb_hyp cty + nmiss | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some p -> snd p | None -> pat
+ in
if Int.equal nmiss 0 then
(Some hd,
- { pri = (match pri with None -> nb_hyp cty | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
+ { pri; poly; pat = Some pat; name;
db = None;
secvars;
code = with_uid (Res_pf(c,cty,ctx)); })
@@ -784,12 +788,8 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
str " will only be used by eauto");
(Some hd,
- { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- db = None;
- secvars;
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
code = with_uid (ERes_pf(c,cty,ctx)); })
end
| _ -> failwith "make_apply_entry"
@@ -840,14 +840,14 @@ let fresh_global_or_constr env sigma poly cr =
(c, Univ.ContextSet.empty)
end
-let make_resolves env sigma flags pri poly ?name cr =
+let make_resolves env sigma flags info poly ?name cr =
let c, ctx = fresh_global_or_constr env sigma poly cr in
let cty = Retyping.get_type_of env sigma c in
let try_apply f =
try Some (f (c, cty, ctx)) with Failure _ -> None in
let ents = List.map_filter try_apply
- [make_exact_entry env sigma pri poly ?name;
- make_apply_entry env sigma flags pri poly ?name]
+ [make_exact_entry env sigma info poly ?name;
+ make_apply_entry env sigma flags info poly ?name]
in
if List.is_empty ents then
errorlabstrm "Hint"
@@ -861,7 +861,7 @@ let make_resolve_hyp env sigma decl =
let hname = get_id decl in
let c = mkVar hname in
try
- [make_apply_entry env sigma (true, true, false) None false
+ [make_apply_entry env sigma (true, true, false) empty_hint_info false
~name:(PathHints [VarRef hname])
(c, get_type decl, Univ.ContextSet.empty)]
with
@@ -1145,16 +1145,17 @@ let add_transparency l b local dbnames =
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_extern pri pat tacast local dbname =
- let pat = match pat with
+let add_extern info tacast local dbname =
+ let pat = match info.hint_pattern with
| None -> None
| Some (_, pat) -> Some pat
in
- let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
+ let hint = make_hint ~local dbname
+ (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
Lib.add_anonymous_leaf (inAutoHint hint)
-let add_externs pri pat tacast local dbnames =
- List.iter (add_extern pri pat tacast local) dbnames
+let add_externs info tacast local dbnames =
+ List.iter (add_extern info tacast local) dbnames
let add_trivials env sigma l local dbnames =
List.iter
@@ -1168,15 +1169,16 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make ()
type hnf = bool
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
+ | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsModeEntry of global_reference * hint_mode list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * glob_tactic_expr
+ | HintsExternEntry of hint_info * glob_tactic_expr
let default_prepare_hint_ident = Id.of_string "H"
@@ -1240,11 +1242,12 @@ let interp_hints poly =
(PathHints [gr], poly, IsGlobRef gr)
| HintsConstr c -> (PathAny, poly, f poly c)
in
- let fres (pri, b, r) =
+ let fp = Constrintern.intern_constr_pattern (Global.env()) in
+ let fres (info, b, r) =
let path, poly, gr = fi r in
- (pri, poly, b, path, gr)
+ let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
+ (info, poly, b, path, gr)
in
- let fp = Constrintern.intern_constr_pattern (Global.env()) in
match h with
| HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
| HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
@@ -1260,14 +1263,14 @@ let interp_hints poly =
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
- None, mib.Declarations.mind_polymorphic, true,
+ empty_hint_info, mib.Declarations.mind_polymorphic, true,
PathHints [gr], IsGlobRef gr)
in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
let pat = Option.map fp patcom in
let l = match pat with None -> [] | Some (l, _) -> l in
let tacexp = Hook.get forward_intern_tac l tacexp in
- HintsExternEntry (pri, pat, tacexp)
+ HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
let add_hints local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
@@ -1283,8 +1286,8 @@ let add_hints local dbnames0 h =
| HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
| HintsTransparencyEntry (lhints, b) ->
add_transparency lhints b local dbnames
- | HintsExternEntry (pri, pat, tacexp) ->
- add_externs pri pat tacexp local dbnames
+ | HintsExternEntry (info, tacexp) ->
+ add_externs info tacexp local dbnames
let expand_constructor_hints env sigma lems =
List.map_append (fun (evd,lem) ->
@@ -1308,7 +1311,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
let lems = expand_constructor_hints env sigma lems in
let hintlist' =
List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply,true,false) None poly lem) lems in
+ make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
Hint_db.add_list env sigma hintlist' hint_db
let make_local_hint_db env sigma ts eapply lems =
@@ -1362,7 +1365,9 @@ let pr_hint h = match h.obj with
(str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
let pr_id_hint (id, v) =
- (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+ let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
+ (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+ ++ str", id " ++ int id ++ str ")" ++ spc ())
let pr_hint_list hintlist =
(str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8145ae193..42a2896ed 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -27,6 +27,8 @@ val decompose_app_bound : constr -> global_reference * constr array
val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+val empty_hint_info : 'a hint_info_gen
+
(** Pre-created hint databases *)
type 'a hint_ast =
@@ -129,20 +131,21 @@ type hint_db = Hint_db.t
type hnf = bool
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
type hint_term =
| IsGlobRef of global_reference
| IsConstr of constr * Univ.universe_context_set
type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom *
- hint_term) list
+ | HintsResolveEntry of
+ (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsModeEntry of global_reference * hint_mode list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+ | HintsExternEntry of hint_info * Tacexpr.glob_tactic_expr
val searchtable_map : hint_db_name -> hint_db
@@ -169,23 +172,34 @@ val prepare_hint : bool (* Check no remaining evars *) ->
(bool * bool) (* polymorphic or monomorphic, local or global *) ->
env -> evar_map -> open_constr -> hint_term
-(** [make_exact_entry pri (c, ctyp, ctx, secvars)].
+(** [make_exact_entry info (c, ctyp, ctx)].
[c] is the term given as an exact proof to solve the goal;
[ctyp] is the type of [c].
- [ctx] is its (refreshable) universe context. *)
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom ->
+ [ctx] is its (refreshable) universe context.
+ In info:
+ [hint_priority] is the hint's desired priority, it is 0 if unspecified
+ [hint_pattern] is the hint's desired pattern, it is inferred if not specified
+*)
+
+val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
(constr * types * Univ.universe_context_set) -> hint_entry
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)].
+(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
[eapply] is true if this hint will be used only with EApply;
[hnf] should be true if we should expand the head of cty before searching for
products;
[c] is the term given as an exact proof to solve the goal;
[cty] is the type of [c].
- [ctx] is its (refreshable) universe context. *)
+ [ctx] is its (refreshable) universe context.
+ In info:
+ [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
+ if unspecified
+ [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty]
+ if not specified
+*)
val make_apply_entry :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
+ env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
(constr * types * Univ.universe_context_set) -> hint_entry
(** A constr which is Hint'ed will be:
@@ -196,7 +210,7 @@ val make_apply_entry :
has missing arguments. *)
val make_resolves :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
+ env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
hint_term -> hint_entry list
(** [make_resolve_hyp hname htyp].
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 89b8bd7ac..91edc06bf 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -8,6 +8,10 @@ Hint Unfold eq_sym: core.
Hint Constructors eq: foo bar.
Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
+Hint Resolve eq_refl | 4 (_ = _) : baz.
+Hint Resolve eq_sym eq_trans : baz.
+Hint Extern 3 (_ = _) => apply eq_sym : baz.
+
(* Old-style syntax *)
Hint Resolve eq_refl eq_sym.
Hint Resolve eq_refl eq_sym: foo.
@@ -105,4 +109,4 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
Timeout 1 Fail apply _. (* 0.06s *)
Abort.
-End HintCut. \ No newline at end of file
+End HintCut.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d6a6162f9..1f13ab637 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -46,25 +46,32 @@ let set_typeclass_transparency c local b =
let _ =
Hook.set Typeclasses.add_instance_hint_hook
- (fun inst path local pri poly ->
+ (fun inst path local info poly ->
let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
| IsGlobal gr -> Hints.IsGlobRef gr
in
- Flags.silently (fun () ->
+ let info =
+ Vernacexpr.{ info with hint_pattern =
+ Option.map
+ (Constrintern.intern_constr_pattern (Global.env())) info.hint_pattern } in
+ Flags.silently (fun () ->
Hints.add_hints local [typeclasses_db]
(Hints.HintsResolveEntry
- [pri, poly, false, Hints.PathHints path, inst'])) ());
+ [info, poly, false, Hints.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook
(fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
-
+
+open Vernacexpr
+
(** TODO: add subinstances *)
-let existing_instance glob g pri =
+let existing_instance glob g info =
let c = global g in
+ let info = Option.default Hints.empty_hint_info info in
let instance = Global.type_of_global_unsafe c in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err_loc (loc_of_reference g, "declare_instance",
Pp.str "Constant does not build instances of a declared type class.")
@@ -98,12 +105,12 @@ let id_of_class cl =
open Pp
-let instance_hook k pri global imps ?hook cst =
+let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
- Typeclasses.declare_instance pri (not global) cst;
+ Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
let kind = IsDefinition Instance in
let evm =
let levels = Univ.LSet.union (Universes.universes_of_constr termtype)
@@ -118,7 +125,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
Universes.register_universe_binders (ConstRef kn) pl;
- instance_hook k pri global imps ?hook (ConstRef kn);
+ instance_hook k info global imps ?hook (ConstRef kn);
id
let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
@@ -130,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let evars = ref (Evd.from_ctx uctx) in
let tclass, ids =
match bk with
- | Implicit ->
+ | Decl_kinds.Implicit ->
Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
(fun avoid (clname, _) ->
match clname with
@@ -299,7 +306,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let hook vis gr _ =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
- Typeclasses.declare_instance pri (not global) (ConstRef cst)
+ Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
let obls, constr, typ =
match term with
@@ -378,7 +385,7 @@ let context poly l =
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr t with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+ add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
poly (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7beb873e6..d2cb788ea 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -20,12 +20,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
(** Instance declaration *)
-val existing_instance : bool -> reference -> int option -> unit
-(** globality, reference, priority *)
+val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+(** globality, reference, optional priority and pattern information *)
val declare_instance_constant :
typeclass ->
- int option -> (** priority *)
+ Vernacexpr.hint_info_expr -> (** priority *)
bool -> (** globality *)
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Globnames.global_reference -> unit) ->
@@ -48,7 +48,7 @@ val new_instance :
?generalize:bool ->
?tac:unit Proofview.tactic ->
?hook:(Globnames.global_reference -> unit) ->
- int option ->
+ Vernacexpr.hint_info_expr ->
Id.t
(** Setting opacity *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9c4d41ea5..63564fba1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -565,8 +565,9 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
let gr = match kind with
- | Class def ->
- let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+ | Class def ->
+ let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
+ let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b09425563..c50e57786 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,8 @@ val declare_structure :
inductive
val definition_structure :
- inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
+ inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
+ plident with_coercion * local_binder list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4de1d9595..973f73ef6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -841,9 +841,9 @@ let vernac_instance abst locality poly sup inst props pri =
let vernac_context poly l =
if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
-let vernac_declare_instances locality ids pri =
+let vernac_declare_instances locality insts =
let glob = not (make_section_locality locality) in
- List.iter (fun id -> Classes.existing_instance glob id pri) ids
+ List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
let vernac_declare_class id =
Record.declare_existing_class (Nametab.global id)
@@ -1989,10 +1989,10 @@ let interp ?proof ~loc locality poly c =
vernac_identity_coercion locality poly local id s t
(* Type classes *)
- | VernacInstance (abst, sup, inst, props, pri) ->
- vernac_instance abst locality poly sup inst props pri
+ | VernacInstance (abst, sup, inst, props, info) ->
+ vernac_instance abst locality poly sup inst props info
| VernacContext sup -> vernac_context poly sup
- | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
+ | VernacDeclareInstances insts -> vernac_declare_instances locality insts
| VernacDeclareClass id -> vernac_declare_class id
(* Solving *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:43:37 +0000