aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli4
-rw-r--r--library/declare.ml11
-rw-r--r--library/declare.mli4
-rw-r--r--library/global.mli1
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--plugins/setoid_ring/Field_theory.v32
-rw-r--r--pretyping/typeclasses.ml20
-rw-r--r--pretyping/typeclasses.mli10
-rw-r--r--printing/ppvernac.ml4
-rw-r--r--tactics/auto.ml34
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--tactics/extratactics.ml419
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/Init/Peano.v18
-rw-r--r--theories/Lists/SetoidList.v14
-rw-r--r--theories/MSets/MSetAVL.v2
-rw-r--r--theories/MSets/MSetGenTree.v2
-rw-r--r--theories/MSets/MSetList.v15
-rw-r--r--theories/MSets/MSetRBT.v2
-rw-r--r--theories/MSets/MSetWeakList.v10
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v53
-rw-r--r--theories/Reals/RIneq.v4
-rw-r--r--toplevel/classes.ml2
24 files changed, 168 insertions, 107 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 31c1643d2..25897950e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -103,8 +103,8 @@ type comment =
| CommentInt of int
type hints_expr =
- | HintsResolve of (int option * bool * constr_expr) list
- | HintsImmediate of constr_expr list
+ | HintsResolve of (int option * bool * reference) list
+ | HintsImmediate of reference list
| HintsUnfold of reference list
| HintsTransparency of reference list * bool
| HintsConstructors of reference list
diff --git a/library/declare.ml b/library/declare.ml
index aa10cf314..7364031d5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -180,6 +180,17 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) =
!xml_declare_constant (internal,kn);
kn
+let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition)
+ id ?types body =
+ let cb =
+ { Entries.const_entry_body = body;
+ const_entry_type = types;
+ const_entry_opaque = opaque;
+ const_entry_secctx = None }
+ in
+ declare_constant ~internal id
+ (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
+
(** Declaration of inductive blocks *)
let declare_inductive_argument_scopes kn mie =
diff --git a/library/declare.mli b/library/declare.mli
index 6f69f673e..9cc6e371c 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -57,6 +57,10 @@ type internal_flag =
val declare_constant :
?internal:internal_flag -> identifier -> constant_declaration -> constant
+val declare_definition :
+ ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
+ identifier -> ?types:constr -> constr -> constant
+
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block (boolean must be true iff it is a record) *)
diff --git a/library/global.mli b/library/global.mli
index ff3c73199..82b7cc8eb 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -101,6 +101,5 @@ val import : compiled_library -> Digest.t -> module_path
val type_of_global : Globnames.global_reference -> types
val env_of_context : Environ.named_context_val -> Environ.env
-
(** spiwack: register/unregister function for retroknowledge *)
val register : Retroknowledge.field -> constr -> constr -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index eee6d3ce6..f2bf542ef 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -91,7 +91,7 @@ GEXTEND Gram
VernacHints (enforce_module_locality local,dbnames, h)
(* Declare "Resolve" explicitly so as to be able to later extend with
"Resolve ->" and "Resolve <-" *)
- | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural;
+ | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference; n = OPT natural;
dbnames = opt_hintbases ->
VernacHints (use_module_locality (),dbnames,
HintsResolve (List.map (fun x -> (n, true, x)) lc))
@@ -101,9 +101,9 @@ GEXTEND Gram
[ [ IDENT "Local" -> true | -> false ] ]
;
hint:
- [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural ->
+ [ [ IDENT "Resolve"; lc = LIST1 global; n = OPT natural ->
HintsResolve (List.map (fun x -> (n, true, x)) lc)
- | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+ | IDENT "Immediate"; lc = LIST1 global -> HintsImmediate lc
| IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
| IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
| IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc05c252c..341c0e6f5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -84,15 +84,29 @@ Qed.
Let eq_trans := Setoid.Seq_trans _ _ Rsth.
Let eq_sym := Setoid.Seq_sym _ _ Rsth.
Let eq_refl := Setoid.Seq_refl _ _ Rsth.
-
-Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
-Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
- (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
-Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth)
- (ARmul_1_l ARth) (ARmul_0_l ARth)
- (ARmul_comm ARth) (ARmul_assoc ARth) (ARdistr_l ARth)
- (ARopp_mul_l ARth) (ARopp_add ARth)
- (ARsub_def ARth) .
+Let mor1h := CRmorph.(morph1).
+
+Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO .
+
+Let lem1 := Rmul_ext Reqe.
+Let lem2 := Rmul_ext Reqe.
+Let lem3 := (Radd_ext Reqe).
+Let lem4 := ARsub_ext Rsth Reqe ARth.
+Let lem5 := Ropp_ext Reqe.
+Let lem6 := ARadd_0_l ARth.
+Let lem7 := ARadd_comm ARth.
+Let lem8 := (ARadd_assoc ARth).
+Let lem9 := ARmul_1_l ARth.
+Let lem10 := (ARmul_0_l ARth).
+Let lem11 := ARmul_comm ARth.
+Let lem12 := ARmul_assoc ARth.
+Let lem13 := (ARdistr_l ARth).
+Let lem14 := ARopp_mul_l ARth.
+Let lem15 := (ARopp_add ARth).
+Let lem16 := ARsub_def ARth.
+
+Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
+ lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
(* Power coefficients *)
Variable Cpow : Type.
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2749538c0..95fdcdfe6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -39,6 +39,11 @@ 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 =
@@ -238,6 +243,12 @@ 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 i = ref (-1) in
+ (fun () -> incr i;
+ Nameops.add_suffix id ("_subinstance_" ^ string_of_int !i))
+ in
let rec aux pri c =
let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
match class_of_constr ty with
@@ -261,10 +272,13 @@ let build_subclasses ~check env sigma glob pri =
| Some p, None -> Some (p + 1)
| _, _ -> None
in
- Some (ConstRef proj, pri, body)) tc.cl_projs
+ let c = !declare_definition_ref ~internal:true
+ ~kind:Decl_kinds.Instance (next_id ()) body
+ in
+ Some (ConstRef proj, pri, ConstRef c)) tc.cl_projs
in
let declare_proj hints (cref, pri, body) =
- let rest = aux pri body in
+ let rest = aux pri (constr_of_global body) in
hints @ (pri, body) :: rest
in List.fold_left declare_proj [] projs
in aux pri (constr_of_global glob)
@@ -313,7 +327,7 @@ let discharge_instance (_, (action, inst)) =
let is_local i = i.is_global = -1
let add_instance check inst =
- add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri;
+ 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)
(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 039aeb1e6..729cbb2ad 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,9 +103,13 @@ 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_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit
+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
val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : constr -> bool -> int option -> unit
+val add_instance_hint : global_reference -> 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
@@ -119,4 +123,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 * constr) list
+ (int option * global_reference) list
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2df8b8ce5..b914e3877 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -185,11 +185,11 @@ let pr_hints local db h pr_c pr_pat =
match h with
| HintsResolve l ->
str "Resolve " ++ prlist_with_sep sep
- (fun (pri, _, c) -> pr_c c ++
+ (fun (pri, _, c) -> pr_reference c ++
match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
l
| HintsImmediate l ->
- str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
+ str"Immediate" ++ spc() ++ prlist_with_sep sep pr_reference l
| HintsUnfold l ->
str "Unfold " ++ prlist_with_sep sep pr_reference l
| HintsTransparency (l, b) ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 47b89e9af..b20caf450 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -560,7 +560,8 @@ let make_extern pri pat tacast =
name = PathAny;
code = Extern tacast })
-let make_trivial env sigma ?(name=PathAny) c =
+let make_trivial env sigma ?(name=PathAny) r =
+ let c = constr_of_global 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
@@ -716,8 +717,9 @@ let add_resolves env sigma clist local dbnames =
Lib.add_anonymous_leaf
(inAutoHint
(local,dbname, AddHints
- (List.flatten (List.map (fun (x, hnf, path, y) ->
- make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
+ (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)))))
dbnames
let add_unfolds l local dbnames =
@@ -772,8 +774,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 * constr) list
- | HintsImmediateEntry of (hints_path_atom * constr) list
+ | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+ | HintsImmediateEntry of (hints_path_atom * global_reference) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
@@ -813,24 +815,19 @@ let prepare_hint env (sigma,c) =
mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
iter c
-let path_of_constr_expr c =
- match c with
- | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny)
- | _ -> PathAny
-
let interp_hints h =
- let f c =
- let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
- let c = prepare_hint (Global.env()) (evd,c) in
- Evarutil.check_evars (Global.env()) Evd.empty evd c;
- c in
let fr r =
let gr = global_with_alias r in
let r' = evaluable_of_global_reference (Global.env()) gr in
Dumpglob.add_glob (loc_of_reference r) gr;
r' in
- let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in
- let fi c = path_of_constr_expr c, f c in
+ let fres (o, b, c) =
+ let gr = global_with_alias c in
+ (o, b, PathHints [gr], gr) in
+ let fi c =
+ let gr = global_with_alias c in
+ PathHints [gr], gr
+ in
let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
match h with
| HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
@@ -843,7 +840,8 @@ let interp_hints h =
let ind = global_inductive_with_alias qid in
Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
List.tabulate (fun i -> let c = (ind,i+1) in
- None, true, PathHints [ConstructRef c], mkConstruct c)
+ let gr = ConstructRef c in
+ None, true, PathHints [gr], 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 094030bea..de1d2ff6b 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 * constr) list
- | HintsImmediateEntry of (hints_path_atom * constr) list
+ | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+ | HintsImmediateEntry of (hints_path_atom * global_reference) 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 1fc013496..f2f5417ef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -250,7 +250,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
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 c)
+ (true,false,Flags.is_verbose()) pri (constr_of_global c))
hints)
else []
in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c2d5de265..1c9833571 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -273,9 +273,10 @@ END
open Term
open Coqlib
-let project_hint pri l2r c =
+let project_hint pri l2r r =
+ let gr = Smartlocate.global_with_alias r in
let env = Global.env() in
- let c = Constrintern.interp_constr Evd.empty env c in
+ let c = Globnames.constr_of_global gr in
let t = Retyping.get_type_of env Evd.empty c in
let t =
Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
@@ -288,24 +289,28 @@ let project_hint pri l2r c =
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
- (pri,true,Auto.PathAny,c)
+ 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)
let add_hints_iff l2r lc n bl =
Auto.add_hints true bl
(Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
VERNAC COMMAND EXTEND HintResolveIffLR
- [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+ [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ add_hints_iff true lc n bl ]
-| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
[ add_hints_iff true lc n ["core"] ]
END
VERNAC COMMAND EXTEND HintResolveIffRL
- [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+ [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ add_hints_iff false lc n bl ]
-| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
[ add_hints_iff false lc n ["core"] ]
END
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 36c328cf4..b8fdac8c9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -56,7 +56,7 @@ Class Asymmetric {A} (R : relation A) :=
Class Transitive {A} (R : relation A) :=
transitivity : forall x y z, R x y -> R y z -> R x z.
-Hint Resolve @irreflexivity : ord.
+Hint Resolve irreflexivity : ord.
Unset Implicit Arguments.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8c6fba508..3c0fc02e4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -30,9 +30,10 @@ Require Import Logic.
Open Scope nat_scope.
Definition eq_S := f_equal S.
+Definition f_equal_nat := f_equal (A:=nat).
-Hint Resolve (f_equal S): v62.
-Hint Resolve (f_equal (A:=nat)): core.
+Hint Resolve eq_S: v62.
+Hint Resolve f_equal_nat: core.
(** The predecessor function *)
@@ -40,7 +41,8 @@ Definition pred (n:nat) : nat := match n with
| O => n
| S u => u
end.
-Hint Resolve (f_equal pred): v62.
+Definition f_equal_pred := f_equal pred.
+Hint Resolve f_equal_pred: v62.
Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
@@ -88,8 +90,10 @@ Fixpoint plus (n m:nat) : nat :=
where "n + m" := (plus n m) : nat_scope.
-Hint Resolve (f_equal2 plus): v62.
-Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+Definition f_equal2_plus := f_equal2 plus.
+Hint Resolve f_equal2_plus: v62.
+Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat).
+Hint Resolve f_equal2_nat: core.
Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
@@ -127,8 +131,8 @@ Fixpoint mult (n m:nat) : nat :=
end
where "n * m" := (mult n m) : nat_scope.
-
-Hint Resolve (f_equal2 mult): core.
+Definition f_equal2_mult := f_equal2 mult.
+Hint Resolve f_equal2_mult: core.
Lemma mult_n_O : forall n:nat, 0 = n * 0.
Proof.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 7d3c383c1..8fd229917 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed.
(** Results concerning lists modulo [eqA] *)
Hypothesis eqA_equiv : Equivalence eqA.
+Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
+Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
+Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
-Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
+Hint Resolve eqarefl eqatrans.
+Hint Immediate eqasym.
Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
@@ -633,7 +635,9 @@ Variable ltA : A -> A -> Prop.
Hypothesis ltA_strorder : StrictOrder ltA.
Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
-Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Hint Resolve sotrans.
Notation InfA:=(lelistA ltA).
Notation SortA:=(sort ltA).
@@ -821,7 +825,7 @@ Arguments eq {A} x _.
Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
Proof.
-clear ltA ltA_compat ltA_strorder.
+clear sotrans ltA ltA_strorder ltA_compat.
intros; do 2 rewrite InA_alt; intuition.
destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 1e66e2b5b..2182504dd 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -306,7 +306,7 @@ Include MSetGenTree.Props X I.
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree Ok.
Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index cacd91343..b7f3f96c9 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -341,7 +341,7 @@ Module Import MX := OrderedTypeFacts X.
Scheme tree_ind := Induction for tree Sort Prop.
Scheme bst_ind := Induction for bst Sort Prop.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree.
Local Hint Constructors InT bst.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d9b1fd9bb..b0e09b719 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -228,16 +228,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Notation Inf := (lelistA X.lt).
Notation In := (InA X.eq).
- (* TODO: modify proofs in order to avoid these hints *)
- Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
- Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
- Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+ Existing Instance X.eq_equiv.
+ Hint Extern 20 => solve [order].
Definition IsOk s := Sort s.
Class Ok (s:t) : Prop := ok : Sort s.
- Hint Resolve @ok.
+ Hint Resolve ok.
Hint Unfold Ok.
Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -343,7 +341,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
induction s; simpl; intros.
intuition. inv; auto.
elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
- left; order.
Qed.
Lemma remove_inf :
@@ -402,8 +399,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
Proof.
repeat rewrite <- isok_iff; revert s s'.
- induction2; constructors; try apply @ok; auto.
- apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+ induction2; constructors; try apply @ok; auto.
+ apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.
change (Inf x' (union (x :: l) l')); auto.
Qed.
@@ -412,7 +409,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
In x (union s s') <-> In x s \/ In x s'.
Proof.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
- left; order.
Qed.
Lemma inter_inf :
@@ -440,7 +436,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
try sort_inf_in; try order.
- left; order.
Qed.
Lemma diff_inf :
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b838495f9..92ad2fcfb 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -452,7 +452,7 @@ Local Notation Bk := (Node Black).
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree Ok.
Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index fd4114cd4..7c8c5e6de 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -118,16 +118,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
Notation In := (InA X.eq).
(* TODO: modify proofs in order to avoid these hints *)
- Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
- Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
- Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+ Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
+ Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
+ Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+ Hint Resolve eqr eqtrans.
+ Hint Immediate eqsym.
Definition IsOk := NoDup.
Class Ok (s:t) : Prop := ok : NoDup s.
Hint Unfold Ok.
- Hint Resolve @ok.
+ Hint Resolve ok.
Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 94d3e97a5..809169a4d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -354,6 +354,8 @@ Section Z_2nZ.
(* Proof *)
Context {specs : ZnZ.Specs ops}.
+
+ Create HintDb ZnZ.
Hint Resolve
ZnZ.spec_to_Z
@@ -397,9 +399,9 @@ Section Z_2nZ.
ZnZ.spec_sqrt
ZnZ.spec_WO
ZnZ.spec_OW
- ZnZ.spec_WW.
-
- Ltac wwauto := unfold ww_to_Z; auto.
+ ZnZ.spec_WW : ZnZ.
+
+ Ltac wwauto := unfold ww_to_Z; eauto with ZnZ.
Let wwB := base _ww_digits.
@@ -414,7 +416,7 @@ Section Z_2nZ.
Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x) (at level 0, x at level 99).
Let spec_ww_to_Z : forall x, 0 <= [| x |] < wwB.
- Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_to_Z w_digits w_to_Z _); wwauto. Qed.
Let spec_ww_of_pos : forall p,
Zpos p = (Z.of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|].
@@ -438,15 +440,15 @@ Section Z_2nZ.
Proof. reflexivity. Qed.
Let spec_ww_1 : [|ww_1|] = 1.
- Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed.
+ Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);wwauto. Qed.
Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1.
- Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);wwauto. Qed.
Let spec_ww_compare :
forall x y, compare x y = Z.compare [|x|] [|y|].
Proof.
- refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto.
+ refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);wwauto.
Qed.
Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0.
@@ -455,14 +457,14 @@ Section Z_2nZ.
Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|].
Proof.
refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _);
- auto.
+ wwauto.
Qed.
Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB.
Proof.
refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp
w_digits w_to_Z _ _ _ _ _);
- auto.
+ wwauto.
Qed.
Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1.
@@ -473,7 +475,7 @@ Section Z_2nZ.
Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1.
Proof.
- refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto.
+ refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);wwauto.
Qed.
Let spec_ww_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|].
@@ -495,7 +497,7 @@ Section Z_2nZ.
Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB.
Proof.
- refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto.
+ refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);wwauto.
Qed.
Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB.
@@ -608,13 +610,14 @@ Section Z_2nZ.
Qed.
Let spec_low: forall x,
- w_to_Z (low x) = [|x|] mod wB.
+ w_to_Z (low x) = [|x|] mod wB.
intros x; case x; simpl low.
- unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto.
+ unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; wwauto.
intros xh xl; simpl.
rewrite Z.add_comm; rewrite Z_mod_plus; auto with zarith.
rewrite Zmod_small; auto with zarith.
- unfold wB, base; auto with zarith.
+ unfold wB, base; eauto with ZnZ zarith.
+ unfold wB, base; eauto with ZnZ zarith.
Qed.
Let spec_ww_digits:
@@ -632,7 +635,7 @@ Section Z_2nZ.
Proof.
refine (spec_ww_head00 w_0 w_0W
w_compare w_head0 w_add2 w_zdigits _ww_zdigits
- w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); auto.
+ w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto.
exact ZnZ.spec_head00.
exact ZnZ.spec_zdigits.
Qed.
@@ -715,7 +718,7 @@ refine
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Proof.
- refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto.
+ refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);wwauto.
Qed.
Let spec_ww_mod_gt : forall a b,
@@ -735,7 +738,7 @@ refine
Let spec_ww_mod : forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|].
Proof.
- refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto.
+ refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);wwauto.
Qed.
Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] ->
@@ -743,7 +746,7 @@ refine
Proof.
refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _
w_0 w_0 w_eq0 w_gcd_gt _ww_digits
- _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+ _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -752,13 +755,13 @@ refine
exact ZnZ.spec_zdigits.
exact spec_ww_add_mul_div.
refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
- _ _);auto.
+ _ _);wwauto.
Qed.
Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
Proof.
refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
- _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+ _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -767,7 +770,7 @@ refine
exact ZnZ.spec_zdigits.
exact spec_ww_add_mul_div.
refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
- _ _);auto.
+ _ _);wwauto.
Qed.
Let spec_ww_is_even : forall x,
@@ -818,6 +821,8 @@ refine
Proof.
unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith.
Qed.
+
+ Hint Transparent ww_to_Z.
Let ww_testbit_high n x y : Z.pos w_digits <= n ->
Z.testbit [|WW x y|] n =
@@ -826,8 +831,8 @@ refine
intros Hn.
assert (E : ZnZ.to_Z x = [|WW x y|] / wB).
{ simpl.
- rewrite Z.div_add_l; auto with zarith.
- now rewrite Z.div_small, Z.add_0_r. }
+ rewrite Z.div_add_l; eauto with ZnZ zarith.
+ now rewrite Z.div_small, Z.add_0_r; wwauto. }
rewrite E.
unfold wB, base. rewrite Z.div_pow2_bits.
- f_equal; auto with zarith.
@@ -842,7 +847,7 @@ refine
assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
{ simpl; symmetry.
rewrite Z.add_comm, Z.mod_add; auto with zarith.
- apply Z.mod_small; auto with zarith. }
+ apply Z.mod_small; eauto with ZnZ zarith. }
rewrite E.
unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 4dea8e07b..bfa975aab 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -409,7 +409,9 @@ Proof.
rewrite Rplus_assoc; rewrite H; ring.
Qed.
-Hint Resolve (f_equal (A:=R)): real.
+Definition f_equal_R := (f_equal (A:=R)).
+
+Hint Resolve f_equal_R : real.
Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
Proof.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5fe3d3f12..38b5703f3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,7 +34,7 @@ let set_typeclass_transparency c local b =
let _ =
Typeclasses.register_add_instance_hint
(fun inst local pri ->
- let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in
+ let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in
Flags.silently (fun () ->
Auto.add_hints local [typeclasses_db]
(Auto.HintsResolveEntry
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 03:52:04 +0000