aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli16
-rw-r--r--tactics/class_tactics.ml7
-rw-r--r--tactics/hints.ml7
-rw-r--r--tactics/hints.mli10
-rw-r--r--vernac/classes.ml16
-rw-r--r--vernac/classes.mli6
-rw-r--r--vernac/pvernac.mli2
-rw-r--r--vernac/vernacexpr.ml10
9 files changed, 41 insertions, 39 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 12a944d32..70588b6ad 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
let typeclasses_unique_solutions = ref false
let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
@@ -80,7 +80,7 @@ type typeclass = {
cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
- cl_projs : (Name.t * (direction * hint_info_expr) option
+ cl_projs : (Name.t * (direction * hint_info) option
* Constant.t option) list;
cl_strict : bool;
@@ -92,7 +92,7 @@ type typeclasses = typeclass Refmap.t
type instance = {
is_class: GlobRef.t;
- is_info: hint_info_expr;
+ is_info: hint_info;
(* Sections where the instance should be redeclared,
None for discard, Some 0 for none. *)
is_global: int option;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2a8e0b874..c78382c82 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
(** This module defines type-classes *)
type typeclass = {
@@ -44,7 +44,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 * hint_info_expr) option * Constant.t option) list;
+ cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list;
(** Whether we use matching or full unification during resolution *)
cl_strict : bool;
@@ -62,7 +62,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance
+val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
@@ -129,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state
val add_instance_hint_hook :
(global_reference_or_constr -> GlobRef.t list ->
- bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
+ bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
- bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
+ bool -> hint_info -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : GlobRef.t -> 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 -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
-val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
+val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
(** Build the subinstances hints for a given typeclass object.
@@ -146,5 +146,5 @@ val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
subinstances and add only the missing ones. *)
val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t ->
- hint_info_expr ->
- (GlobRef.t list * hint_info_expr * constr) list
+ hint_info ->
+ (GlobRef.t list * hint_info * constr) list
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3e08c6d87..1ddb1a2bf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -546,12 +546,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
(List.map_append
(fun (path,info,c) ->
- let info =
- { info with hint_pattern =
- Option.map (Constrintern.intern_constr_pattern env sigma)
- info.hint_pattern }
- in
- make_resolves env sigma ~name:(PathHints path)
+ make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info false
(IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
hints)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b5be4c1c..40cbfa5ab 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Libobject
open Namegen
open Libnames
open Smartlocate
-open Misctypes
open Termops
open Inductiveops
open Typing
@@ -100,6 +99,8 @@ let empty_hint_info =
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -165,7 +166,7 @@ type hint_mode =
| ModeOutput (* Anything *)
type hints_expr =
- | HintsResolve of (Typeclasses.hint_info_expr * 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
@@ -1235,7 +1236,7 @@ let add_trivials env sigma l local dbnames =
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type nonrec hint_info = hint_info
type hints_entry =
| HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f05988703..7ef7f0185 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -14,10 +14,10 @@ open EConstr
open Environ
open Decl_kinds
open Evd
-open Misctypes
open Tactypes
open Clenv
open Pattern
+open Typeclasses
(** {6 General functions. } *)
@@ -33,6 +33,8 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen
(** Pre-created hint databases *)
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -80,7 +82,7 @@ type hint_mode =
| ModeOutput (* Anything *)
type hints_expr =
- | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
| HintsImmediate of reference_or_constr list
| HintsUnfold of Libnames.reference list
| HintsTransparency of Libnames.reference list * bool
@@ -160,8 +162,6 @@ type hint_db = Hint_db.t
type hnf = bool
-type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
-
type hint_term =
| IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
@@ -290,3 +290,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t
(** Hook for changing the initialization of auto *)
val add_hints_init : (unit -> unit) -> unit
+type nonrec hint_info = hint_info
+[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]
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 cf0da4de2..40fab1f9c 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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 10:12:48 +0000