aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/globnames.ml8
-rw-r--r--library/globnames.mli6
-rw-r--r--pretyping/typeclasses.ml36
-rw-r--r--pretyping/typeclasses.mli11
-rw-r--r--tactics/auto.ml32
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/class_tactics.ml44
-rw-r--r--tactics/extratactics.ml46
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v2
-rw-r--r--toplevel/classes.ml6
10 files changed, 59 insertions, 56 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 81cb241c9..b5312e574 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -128,6 +128,14 @@ module ExtRefOrdered = struct
| _, _ -> Pervasives.compare x y
end
+type global_reference_or_constr =
+ | IsGlobal of global_reference
+ | IsConstr of constr
+
+let constr_of_global_or_constr = function
+ | IsConstr c -> c
+ | IsGlobal gr -> constr_of_global gr
+
(** {6 Temporary function to brutally form kernel names from section paths } *)
let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
diff --git a/library/globnames.mli b/library/globnames.mli
index 02ac51fb1..af1f10ee4 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -72,6 +72,12 @@ module ExtRefOrdered : sig
val compare : t -> t -> int
end
+type global_reference_or_constr =
+ | IsGlobal of global_reference
+ | IsConstr of constr
+
+val constr_of_global_or_constr : global_reference_or_constr -> constr
+
(** {6 Temporary function to brutally form kernel names from section paths } *)
val encode_mind : dir_path -> identifier -> mutual_inductive
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7d9d0bbd8..b5c710da2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -20,7 +20,7 @@ open Libobject
(*i*)
-let add_instance_hint_ref = ref (fun id local pri -> assert false)
+let add_instance_hint_ref = ref (fun id path local pri -> assert false)
let register_add_instance_hint =
(:=) add_instance_hint_ref
let add_instance_hint id = !add_instance_hint_ref id
@@ -39,11 +39,6 @@ let classes_transparent_state_ref = ref (fun () -> assert false)
let register_classes_transparent_state = (:=) classes_transparent_state_ref
let classes_transparent_state () = !classes_transparent_state_ref ()
-
-let declare_definition_ref = ref (fun ?internal ?opaque ?kind id ?types constr -> assert false)
-let register_declare_definition =
- (:=) declare_definition_ref
-
let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
let resolve_one_typeclass env evm t =
@@ -247,18 +242,20 @@ let check_instance env sigma c =
with _ -> false
let build_subclasses ~check env sigma glob pri =
- let id = Nametab.basename_of_global glob in
- let next_id =
+ let _id = Nametab.basename_of_global glob in
+ let _next_id =
let i = ref (-1) in
(fun () -> incr i;
- Nameops.add_suffix id ("_subinstance_" ^ string_of_int !i))
+ Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
in
- let rec aux pri c =
+ let rec aux pri c path =
let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
match class_of_constr ty with
| None -> []
| Some (rels, (tc, args)) ->
- let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in
+ let instapp =
+ Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels))
+ in
let projargs = Array.of_list (args @ [instapp]) in
let projs = List.map_filter
(fun (n, b, proj) ->
@@ -276,16 +273,14 @@ let build_subclasses ~check env sigma glob pri =
| Some p, None -> Some (p + 1)
| _, _ -> None
in
- let c = !declare_definition_ref ~internal:true
- ~kind:Decl_kinds.Instance (next_id ()) body
- in
- Some (ConstRef proj, pri, ConstRef c)) tc.cl_projs
+ Some (ConstRef proj, pri, body)) tc.cl_projs
in
let declare_proj hints (cref, pri, body) =
- let rest = aux pri (constr_of_global body) in
- hints @ (pri, body) :: rest
+ let path' = cref :: path in
+ let rest = aux pri body path' in
+ hints @ (path', pri, body) :: rest
in List.fold_left declare_proj [] projs
- in aux pri (constr_of_global glob)
+ in aux pri (constr_of_global glob) [glob]
(*
* instances persistent object
@@ -331,8 +326,9 @@ let discharge_instance (_, (action, inst)) =
let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
- add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
- List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri)
+ add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) inst.is_pri;
+ List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
+ (is_local inst) pri)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
(Global.env ()) Evd.empty inst.is_impl inst.is_pri)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 729cbb2ad..72b3bbd27 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,13 +103,12 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
val register_classes_transparent_state : (unit -> transparent_state) -> unit
val classes_transparent_state : unit -> transparent_state
-val register_declare_definition : (?internal:bool -> ?opaque:bool -> ?kind:definition_object_kind -> identifier -> ?types:constr -> constr -> constant) -> unit
-
-
val register_add_instance_hint :
- (global_reference -> bool (* local? *) -> int option -> unit) -> unit
+ (global_reference_or_constr -> global_reference list ->
+ bool (* local? *) -> int option -> unit) -> unit
val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : global_reference -> bool -> int option -> unit
+val add_instance_hint : global_reference_or_constr -> global_reference list ->
+ bool -> int option -> unit
val remove_instance_hint : global_reference -> unit
val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
@@ -123,4 +122,4 @@ val declare_instance : int option -> bool -> global_reference -> unit
subinstances and add only the missing ones. *)
val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
- (int option * global_reference) list
+ (global_reference list * int option * constr) list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b626e662d..a462460a5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -574,10 +574,10 @@ let make_extern pri pat tacast =
{ pri = pri;
pat = pat;
name = PathAny;
- code = Extern tacast })
+ code = Extern tacast })
let make_trivial env sigma ?(name=PathAny) r =
- let c = constr_of_global r in
+ let c = constr_of_global_or_constr r in
let t = hnf_constr env sigma (type_of env sigma c) in
let hd = head_of_constr_reference (fst (head_constr t)) in
let ce = mk_clenv_from dummy_goal (c,t) in
@@ -726,6 +726,8 @@ let remove_hints local dbnames grs =
Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
dbnames
+open Misctypes
+
(**************************************************************************)
(* The "Hint" vernacular command *)
(**************************************************************************)
@@ -736,8 +738,12 @@ let add_resolves env sigma clist local dbnames =
(inAutoHint
(local,dbname, AddHints
(List.flatten (List.map (fun (x, hnf, path, gr) ->
- make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path
- (constr_of_global gr)) clist)))))
+ let c =
+ match gr with
+ | IsConstr c -> c
+ | IsGlobal gr -> constr_of_global gr
+ in
+ make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path c) clist)))))
dbnames
let add_unfolds l local dbnames =
@@ -792,8 +798,8 @@ let forward_intern_tac =
let set_extern_intern_tac f = forward_intern_tac := f
type hints_entry =
- | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
- | HintsImmediateEntry of (hints_path_atom * global_reference) list
+ | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
+ | HintsImmediateEntry of (hints_path_atom * global_reference_or_constr) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
@@ -834,7 +840,6 @@ let prepare_hint env (sigma,c) =
iter c
let interp_hints =
- let hint_counter = ref 1 in
fun h ->
let f c =
let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
@@ -850,15 +855,8 @@ let interp_hints =
match c with
| HintsReference c ->
let gr = global_with_alias c in
- (PathHints [gr], gr)
- | HintsConstr c ->
- let term = f c in
- let id = id_of_string ("auto_hint_" ^ string_of_int !hint_counter) in
- incr hint_counter;
- let kn = Declare.declare_definition ~internal:Declare.KernelSilent
- ~opaque:false id term in
- let gr = ConstRef kn in
- (PathHints [gr], gr)
+ (PathHints [gr], IsGlobal gr)
+ | HintsConstr c -> (PathAny, IsConstr (f c))
in
let fres (o, b, c) =
let path, gr = fi c in
@@ -877,7 +875,7 @@ let interp_hints =
Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
List.tabulate (fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
- None, true, PathHints [gr], gr)
+ None, true, PathHints [gr], IsGlobal gr)
(nconstructors ind) in
HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index de1d2ff6b..b7f5a312a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -96,8 +96,8 @@ type hint_db_name = string
type hint_db = Hint_db.t
type hints_entry =
- | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
- | HintsImmediateEntry of (hints_path_atom * global_reference) list
+ | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
+ | HintsImmediateEntry of (hints_path_atom * global_reference_or_constr) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bc2e8ac2b..a18992f70 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -249,8 +249,8 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
if is_class then
let hints = build_subclasses ~check:false env sigma (VarRef id) None in
(List.map_append
- (fun (pri, c) -> make_resolves env sigma
- (true,false,Flags.is_verbose()) pri (constr_of_global c))
+ (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
+ (true,false,Flags.is_verbose()) pri c)
hints)
else []
in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 4e22044d5..ade53e768 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -289,11 +289,7 @@ let project_hint pri l2r r =
let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
let c = it_mkLambda_or_LetIn
(mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
- let id =
- Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
- in
- let c = Declare.declare_definition ~internal:Declare.KernelSilent id c in
- (pri,true,Auto.PathAny, Globnames.ConstRef c)
+ (pri,true,Auto.PathAny, Globnames.IsConstr c)
let add_hints_iff l2r lc n bl =
Auto.add_hints true bl
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 40556c4aa..df5d42bbc 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -761,7 +761,7 @@ intros x; case x; simpl ww_is_even.
auto.
split.
unfold zn2z_to_Z; rewrite <- Hw1.
- unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1.
+ unfold ww_to_Z, zn2z_to_Z in H1. rewrite H1.
rewrite <- Hw0.
match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U =>
transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 43caf3fa3..618ec2bc0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -24,6 +24,7 @@ open Constrexpr
open Decl_kinds
open Entries
+open Misctypes
let typeclasses_db = "typeclass_instances"
@@ -33,12 +34,11 @@ let set_typeclass_transparency c local b =
let _ =
Typeclasses.register_add_instance_hint
- (fun inst local pri ->
- let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in
+ (fun inst path local pri ->
Flags.silently (fun () ->
Auto.add_hints local [typeclasses_db]
(Auto.HintsResolveEntry
- [pri, false, path, inst])) ());
+ [pri, false, Auto.PathHints path, inst])) ());
Typeclasses.register_set_typeclass_transparency set_typeclass_transparency;
Typeclasses.register_classes_transparent_state
(fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 23:15:34 +0000