diff options
| author | Maxime Dénès | 2018-11-13 16:39:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-14 08:53:03 +0100 |
| commit | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (patch) | |
| tree | e51a9b33352681751c8eb67ca37fd8d4bd3033e1 | |
| parent | 94494770254bec236f2f6fe727ae42b79192afe4 (diff) | |
Deprecate hint declaration/removal with no specified database
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
58 files changed, 305 insertions, 286 deletions
diff --git a/CHANGES.md b/CHANGES.md index c830bc7a1c..c5f6d55ac7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -47,6 +47,10 @@ Tactics (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted the same way as other variable names occurring in Ltac functions. +- Hint declaration and removal should now specify a database (e.g. `Hint Resolve + foo : database`). When the database name is omitted, the hint is added to the + core database (as previously), but a deprecation warning is emitted. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index f1095fc9f1..638a4cef21 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -10,7 +10,7 @@ end. Arguments decide P /H. -Hint Extern 5 => progress bool. +Hint Extern 5 => progress bool : core. Ltac define t x H := set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x. @@ -147,7 +147,7 @@ Qed. (** * The core reflexive part. *) -Hint Constructors valid. +Hint Constructors valid : core. Fixpoint beq_poly pl pr := match pl with @@ -315,7 +315,7 @@ Section Validity. (* Decision procedure of validity *) -Hint Constructors valid linear. +Hint Constructors valid linear : core. Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p. Proof. @@ -425,10 +425,10 @@ match goal with | [ |- (?z < Pos.max ?x ?y)%positive ] => apply Pos.max_case_strong; intros; lia | _ => zify; omega -end. -Hint Resolve Pos.le_max_r Pos.le_max_l. +end : core. +Hint Resolve Pos.le_max_r Pos.le_max_l : core. -Hint Constructors valid linear. +Hint Constructors valid linear : core. (* Compatibility of validity w.r.t algebraic operations *) diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 4cde08872f..98f5ab067a 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. -Hint Extern 5 => change 0 with (min 0 0). -Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat. -Local Hint Constructors valid. -Hint Extern 5 => zify; omega. +Hint Extern 5 => change 0 with (min 0 0) : core. +Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. +Local Hint Constructors valid : core. +Hint Extern 5 => zify; omega : core. (* Compatibility with validity *) diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index a618fc781f..3a7cf41d43 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr. Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. -Hint Resolve is_true_true not_false_is_true is_true_locked_true. +Hint Resolve is_true_true not_false_is_true is_true_locked_true : core. (** Shorter names. **) Definition isT := is_true_true. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index e2c0ed7c8b..6535cad8b7 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -398,7 +398,7 @@ End ExtensionalEquality. Typeclasses Opaque eqfun. Typeclasses Opaque eqrel. -Hint Resolve frefl rrefl. +Hint Resolve frefl rrefl : core. Notation "f1 =1 f2" := (eqfun f1 f2) (at level 70, no associativity) : fun_scope. diff --git a/tactics/hints.ml b/tactics/hints.ml index 2f2d32e887..328d57c8a3 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1373,10 +1373,10 @@ let interp_hints poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local dbnames0 h = - if String.List.mem "nocore" dbnames0 then +let add_hints ~local dbnames h = + if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); - let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in + assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 42af3583d4..075288e216 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -48,7 +48,7 @@ Proof. discriminate. Qed. Hint Resolve diff_false_true : bool. -Hint Extern 1 (false <> true) => exact diff_false_true. +Hint Extern 1 (false <> true) => exact diff_false_true : core. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. Proof. @@ -621,7 +621,7 @@ Lemma absurd_eq_true : forall b, False -> b = true. Proof. contradiction. Qed. -Hint Resolve absurd_eq_true. +Hint Resolve absurd_eq_true : core. (* A specific instance of eq_trans that preserves compatibility with old hint bool_2 *) @@ -630,7 +630,7 @@ Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z. Proof. apply eq_trans. Qed. -Hint Resolve trans_eq_bool. +Hint Resolve trans_eq_bool : core. (*****************************************) (** * Reflection of [bool] into [Prop] *) diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7af2b0fc45..3e6358c8f3 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -157,6 +157,6 @@ Section RelProd_Instances. Proof. unfold RelCompFun; firstorder. Qed. End RelProd_Instances. -Hint Unfold RelProd RelCompFun. -Hint Extern 2 (RelProd _ _ _ _) => split. +Hint Unfold RelProd RelCompFun : core. +Hint Extern 2 (RelProd _ _ _ _) => split : core. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index b0d1824827..8fc04d81e6 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -41,7 +41,7 @@ Local Open Scope Int_scope. Local Notation int := I.t. Definition key := X.t. -Hint Transparent key. +Hint Transparent key : core. (** * Trees *) @@ -488,8 +488,8 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop. (** * Automation and dedicated tactics. *) -Hint Constructors tree MapsTo In bst. -Hint Unfold lt_tree gt_tree. +Hint Constructors tree MapsTo In bst : core. +Hint Unfold lt_tree gt_tree : core. Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) "as" ident(s) := @@ -569,7 +569,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m. Proof. induction 1; auto. Qed. -Hint Resolve MapsTo_In. +Hint Resolve MapsTo_In : core. Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m. Proof. @@ -588,7 +588,7 @@ Lemma MapsTo_1 : Proof. induction m; simpl; intuition_in; eauto. Qed. -Hint Immediate MapsTo_1. +Hint Immediate MapsTo_1 : core. Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. @@ -627,7 +627,7 @@ Proof. unfold gt_tree in *; intuition_in; order. Qed. -Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. +Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. Lemma lt_left : forall x y l r e h, lt_tree x (Node l y e r h) -> lt_tree x l. @@ -653,7 +653,7 @@ Proof. intuition_in. Qed. -Hint Resolve lt_left lt_right gt_left gt_right. +Hint Resolve lt_left lt_right gt_left gt_right : core. Lemma lt_tree_not_in : forall x m, lt_tree x m -> ~ In x m. @@ -679,7 +679,7 @@ Proof. eauto. Qed. -Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. +Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. (** * Empty map *) @@ -811,7 +811,7 @@ Lemma create_bst : Proof. unfold create; auto. Qed. -Hint Resolve create_bst. +Hint Resolve create_bst : core. Lemma create_in : forall l x e r y, @@ -828,7 +828,7 @@ Proof. (apply lt_tree_node || apply gt_tree_node); auto; (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. -Hint Resolve bal_bst. +Hint Resolve bal_bst : core. Lemma bal_in : forall l x e r y, In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r. @@ -869,7 +869,7 @@ Proof. apply MX.eq_lt with x; auto. apply MX.lt_eq with x; auto. Qed. -Hint Resolve add_bst. +Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. @@ -949,7 +949,7 @@ Proof. destruct 1. apply H2; intuition. Qed. -Hint Resolve remove_min_bst. +Hint Resolve remove_min_bst : core. Lemma remove_min_gt_tree : forall l x e r h, bst (Node l x e r h) -> @@ -968,7 +968,7 @@ Proof. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. -Hint Resolve remove_min_gt_tree. +Hint Resolve remove_min_gt_tree : core. Lemma remove_min_find : forall l x e r h y, bst (Node l x e r h) -> @@ -1120,7 +1120,7 @@ Proof. intuition; [ apply MX.lt_eq with x | ]; eauto. intuition; [ apply MX.eq_lt with x | ]; eauto. Qed. -Hint Resolve join_bst. +Hint Resolve join_bst : core. Lemma join_find : forall l x d r y, bst l -> bst r -> lt_tree x l -> gt_tree x r -> @@ -1256,7 +1256,7 @@ Proof. rewrite remove_min_in, e1; simpl; auto. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. -Hint Resolve concat_bst. +Hint Resolve concat_bst : core. Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> @@ -1344,7 +1344,7 @@ Proof. intros; unfold elements; apply elements_aux_sort; auto. intros; inversion H0. Qed. -Hint Resolve elements_sort. +Hint Resolve elements_sort : core. Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s). Proof. @@ -1612,7 +1612,7 @@ destruct (map_option_2 H) as (d0 & ? & ?). destruct (map_option_2 H') as (d0' & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed. -Hint Resolve map_option_bst. +Hint Resolve map_option_bst : core. Ltac nonify e := replace e with (@None elt) by @@ -1711,7 +1711,7 @@ apply X.lt_trans with x1. destruct (map2_opt_2 H1 H6 Hy); intuition. destruct (map2_opt_2 H2 H7 Hy'); intuition. Qed. -Hint Resolve map2_opt_bst. +Hint Resolve map2_opt_bst : core. Ltac map2_aux := match goal with @@ -2066,7 +2066,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; P.MX.elim_comp; auto. Qed. - Hint Resolve cons_Cmp. + Hint Resolve cons_Cmp : core. Lemma compare_end_Cmp : forall e2, Cmp (compare_end e2) nil (P.flatten_e e2). diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 2d5a79838a..d19c5558d8 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -20,7 +20,7 @@ Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Hint Extern 1 (Equivalence _) => constructor; congruence. +Hint Extern 1 (Equivalence _) => constructor; congruence : core. (** * Facts about weak maps *) diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index c0db8646c7..950b30ee4d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -63,7 +63,7 @@ Inductive avl : t elt -> Prop := (** * Automation and dedicated tactics about [avl]. *) -Hint Constructors avl. +Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. @@ -100,7 +100,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r -> Proof. intros; auto. Qed. -Hint Resolve avl_node. +Hint Resolve avl_node : core. (** Results about [height] *) @@ -193,7 +193,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m). Proof. intros; generalize (add_avl_1 x e H); intuition. Qed. -Hint Resolve add_avl. +Hint Resolve add_avl : core. (** * Extraction of minimum binding *) @@ -274,7 +274,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m). Proof. intros; generalize (remove_avl_1 x H); intuition. Qed. -Hint Resolve remove_avl. +Hint Resolve remove_avl : core. (** * Join *) @@ -331,7 +331,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r). Proof. intros; destruct (join_avl_1 x d H H0); auto. Qed. -Hint Resolve join_avl. +Hint Resolve join_avl : core. (** concat *) @@ -341,7 +341,7 @@ Proof. intros; apply join_avl; auto. generalize (remove_min_avl H0); rewrite e1; simpl; auto. Qed. -Hint Resolve concat_avl. +Hint Resolve concat_avl : core. (** split *) @@ -355,7 +355,7 @@ Proof. Qed. End Elt. -Hint Constructors avl. +Hint Constructors avl : core. Section Map. Variable elt elt' : Type. @@ -713,7 +713,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; MX.elim_comp; auto. Qed. - Hint Resolve cons_Cmp. + Hint Resolve cons_Cmp : core. Lemma compare_aux_Cmp : forall e, Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)). diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 38a96dc393..8970529103 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -58,7 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. Module Type WSfun (E : DecidableType). Definition key := E.t. - Hint Transparent key. + Hint Transparent key : core. Parameter t : Type -> Type. (** the abstract type of maps *) diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 3e98d11976..6ca158a277 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -51,7 +51,7 @@ Proof. intro abs. inversion abs. Qed. -Hint Resolve empty_1. +Hint Resolve empty_1 : core. Lemma empty_sorted : Sort empty. Proof. @@ -216,7 +216,7 @@ Proof. compute in H0,H1. simpl; case (X.compare x x''); intuition. Qed. -Hint Resolve add_Inf. +Hint Resolve add_Inf : core. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). Proof. @@ -302,7 +302,7 @@ Proof. inversion_clear Hm. apply Inf_lt with (x'',e''); auto. Qed. -Hint Resolve remove_Inf. +Hint Resolve remove_Inf : core. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). Proof. @@ -586,7 +586,7 @@ Proof. inversion_clear H; auto. Qed. -Hint Resolve map_lelistA. +Hint Resolve map_lelistA : core. Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'), sort (@ltk elt') (map f m). @@ -654,7 +654,7 @@ Proof. inversion_clear H; auto. Qed. -Hint Resolve mapi_lelistA. +Hint Resolve mapi_lelistA : core. Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'), sort (@ltk elt') (mapi f m). @@ -781,7 +781,7 @@ Proof. inversion_clear H; auto. inversion_clear H0; auto. Qed. -Hint Resolve combine_lelistA. +Hint Resolve combine_lelistA : core. Lemma combine_sorted : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m'), diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 6736096509..03dce9666d 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -49,7 +49,7 @@ Proof. inversion abs. Qed. -Hint Resolve empty_1. +Hint Resolve empty_1 : core. Lemma empty_NoDup : NoDupA empty. Proof. @@ -621,7 +621,7 @@ Proof. inversion_clear 1. intros; apply add_NoDup; auto. Qed. -Hint Resolve fold_right_pair_NoDup. +Hint Resolve fold_right_pair_NoDup : core. Lemma combine_NoDup : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 0c4ecb1f31..3952c28061 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -137,7 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder. Qed. - Hint Resolve compat_P_aux. + Hint Resolve compat_P_aux : core. Definition filter : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), @@ -467,7 +467,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Proof. intros; unfold elements; case (M.elements s); firstorder. Qed. - Hint Resolve elements_3. + Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). Proof. auto. Qed. @@ -666,7 +666,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. rewrite <- H1; firstorder. Qed. - Hint Resolve compat_P_aux. + Hint Resolve compat_P_aux : core. Definition filter (f : elt -> bool) (s : t) : t := let (s', _) := filter (P:=fun x => f x = true) (f_dec f) s in s'. diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 0926d3ae9f..fa7f1c5f4e 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -253,7 +253,7 @@ Module Type WSfun (E : DecidableType). End Spec. - Hint Transparent elt. + Hint Transparent elt : core. Hint Resolve mem_1 equal_1 subset_1 empty_1 is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c9cfb94ace..17f0e25e7a 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -21,8 +21,8 @@ Require Import DecidableTypeEx FSetFacts FSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose compat_op Proper respectful. -Hint Extern 1 (Equivalence _) => constructor; congruence. +Hint Unfold transpose compat_op Proper respectful : core. +Hint Extern 1 (Equivalence _) => constructor; congruence : core. (** First, a functor for Weak Sets in functorial version. *) @@ -732,7 +732,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; rewrite cardinal_Empty; auto. Qed. - Hint Resolve cardinal_inv_1. + Hint Resolve cardinal_inv_1 : core. Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }. @@ -769,7 +769,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). exact Equal_cardinal. Qed. - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. (** ** Cardinal and set operators *) @@ -887,7 +887,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). auto with set. Qed. - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. End WProperties_fun. @@ -952,7 +952,7 @@ Module OrdProperties (M:S). red; intros x a b H; unfold leb. f_equal; apply gtb_compat; auto. Qed. - Hint Resolve gtb_compat leb_compat. + Hint Resolve gtb_compat leb_compat : core. Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 75f14bb4da..7f0387dd12 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -136,7 +136,7 @@ Defined. Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecT : P -> BoolSpec P Q true | BoolSpecF : Q -> BoolSpec P Q false. -Hint Constructors BoolSpec. +Hint Constructors BoolSpec : core. (********************************************************************) @@ -344,7 +344,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. -Hint Constructors CompareSpec. +Hint Constructors CompareSpec : core. (** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a @@ -354,7 +354,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. -Hint Constructors CompareSpecT. +Hint Constructors CompareSpecT : core. Lemma CompareSpec2Type : forall Peq Plt Pgt c, CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. @@ -371,7 +371,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := CompareSpecT (eq x y) (lt x y) (lt y x). -Hint Unfold CompSpec CompSpecT. +Hint Unfold CompSpec CompSpecT : core. Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 4614d215eb..d5241e622c 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -219,7 +219,7 @@ Section Facts. Proof. auto using app_assoc. Qed. - Hint Resolve app_assoc_reverse. + Hint Resolve app_assoc_reverse : core. (* end hide *) (** [app] commutes with [cons] *) @@ -1569,19 +1569,19 @@ Section SetIncl. Variable A : Type. Definition incl (l m:list A) := forall a:A, In a l -> In a m. - Hint Unfold incl. + Hint Unfold incl : core. Lemma incl_refl : forall l:list A, incl l l. Proof. auto. Qed. - Hint Resolve incl_refl. + Hint Resolve incl_refl : core. Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). Proof. auto with datatypes. Qed. - Hint Immediate incl_tl. + Hint Immediate incl_tl : core. Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. Proof. @@ -1592,13 +1592,13 @@ Section SetIncl. Proof. auto with datatypes. Qed. - Hint Immediate incl_appl. + Hint Immediate incl_appl : core. Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). Proof. auto with datatypes. Qed. - Hint Immediate incl_appr. + Hint Immediate incl_appr : core. Lemma incl_cons : forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. @@ -1613,7 +1613,7 @@ Section SetIncl. now_show (In a0 l -> In a0 m). auto. Qed. - Hint Resolve incl_cons. + Hint Resolve incl_cons : core. Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. @@ -1621,7 +1621,7 @@ Section SetIncl. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. - Hint Resolve incl_app. + Hint Resolve incl_app : core. End SetIncl. @@ -2180,7 +2180,7 @@ Section Exists_Forall. | Exists_cons_hd : forall x l, P x -> Exists (x::l) | Exists_cons_tl : forall x l, Exists l -> Exists (x::l). - Hint Constructors Exists. + Hint Constructors Exists : core. Lemma Exists_exists (l:list A) : Exists l <-> (exists x, In x l /\ P x). @@ -2214,7 +2214,7 @@ Section Exists_Forall. | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). - Hint Constructors Forall. + Hint Constructors Forall : core. Lemma Forall_forall (l:list A): Forall l <-> (forall x, In x l -> P x). @@ -2299,8 +2299,8 @@ Section Exists_Forall. End Exists_Forall. -Hint Constructors Exists. -Hint Constructors Forall. +Hint Constructors Exists : core. +Hint Constructors Forall : core. Section Forall2. @@ -2314,7 +2314,7 @@ Section Forall2. | Forall2_cons : forall x y l l', R x y -> Forall2 l l' -> Forall2 (x::l) (y::l'). - Hint Constructors Forall2. + Hint Constructors Forall2 : core. Theorem Forall2_refl : Forall2 [] []. Proof. intros; apply Forall2_nil. Qed. @@ -2348,7 +2348,7 @@ Section Forall2. Qed. End Forall2. -Hint Constructors Forall2. +Hint Constructors Forall2 : core. Section ForallPairs. @@ -2369,7 +2369,7 @@ Section ForallPairs. | FOP_cons : forall a l, Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l). - Hint Constructors ForallOrdPairs. + Hint Constructors ForallOrdPairs : core. Lemma ForallOrdPairs_In : forall l, ForallOrdPairs l -> diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index cc7d6f5536..3afdd8df27 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -193,7 +193,7 @@ Section first_definitions. | auto with datatypes ]. Qed. - Hint Resolve set_add_intro1 set_add_intro2. + Hint Resolve set_add_intro1 set_add_intro2 : core. Lemma set_add_intro : forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x). @@ -224,7 +224,7 @@ Section first_definitions. case H1; trivial. Qed. - Hint Resolve set_add_intro set_add_elim set_add_elim2. + Hint Resolve set_add_intro set_add_elim set_add_elim2 : core. Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. Proof. @@ -310,7 +310,7 @@ Section first_definitions. intros; elim H0; auto with datatypes. Qed. - Hint Resolve set_union_intro2 set_union_intro1. + Hint Resolve set_union_intro2 set_union_intro1 : core. Lemma set_union_intro : forall (a:A) (x y:set), @@ -393,7 +393,7 @@ Section first_definitions. eauto with datatypes. Qed. - Hint Resolve set_inter_elim1 set_inter_elim2. + Hint Resolve set_inter_elim1 set_inter_elim2 : core. Lemma set_inter_elim : forall (a:A) (x y:set), @@ -471,7 +471,7 @@ Section first_definitions. apply (set_diff_elim1 _ _ _ H). Qed. -Hint Resolve set_diff_intro set_diff_trivial. +Hint Resolve set_diff_intro set_diff_trivial : core. End first_definitions. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0c5fe55b27..cab4c23df1 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -30,7 +30,7 @@ Inductive InA (x : A) : list A -> Prop := | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l) | InA_cons_tl : forall y l, InA x l -> InA x (y :: l). -Hint Constructors InA. +Hint Constructors InA : core. (** TODO: it would be nice to have a generic definition instead of the previous one. Having [InA = Exists eqA] raises too @@ -62,7 +62,7 @@ Inductive NoDupA : list A -> Prop := | NoDupA_nil : NoDupA nil | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l). -Hint Constructors NoDupA. +Hint Constructors NoDupA : core. (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *) @@ -93,7 +93,7 @@ Inductive eqlistA : list A -> list A -> Prop := | eqlistA_cons : forall x x' l l', eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l'). -Hint Constructors eqlistA. +Hint Constructors eqlistA : core. (** We could also have written [eqlistA = Forall2 eqA]. *) @@ -107,8 +107,8 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). -Hint Resolve eqarefl eqatrans. -Hint Immediate eqasym. +Hint Resolve eqarefl eqatrans : core. +Hint Immediate eqasym : core. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -154,14 +154,14 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. intros l x y H H'. rewrite <- H. auto. Qed. -Hint Immediate InA_eqA. +Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. simple induction l; simpl; intuition. subst; auto. Qed. -Hint Resolve In_InA. +Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. @@ -786,12 +786,12 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). -Hint Resolve sotrans. +Hint Resolve sotrans : core. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). -Hint Constructors lelistA sort. +Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. @@ -814,7 +814,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. Proof using eqA_equiv ltA_compat. intros H; now rewrite H. Qed. -Hint Immediate InfA_ltA InfA_eqA. +Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. @@ -1005,7 +1005,7 @@ Qed. End Filter. End Type_with_equality. -Hint Constructors InA eqlistA NoDupA sort lelistA. +Hint Constructors InA eqlistA NoDupA sort lelistA : core. Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _. Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _. diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index 24b96514fd..f5ea303343 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -28,7 +28,7 @@ Inductive PermutationA : list A -> list A -> Prop := | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l) | permA_trans l₁ l₂ l₃ : PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃. -Local Hint Constructors PermutationA. +Local Hint Constructors PermutationA : core. Global Instance: Equivalence PermutationA. Proof. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 25b7811417..3914f44a2c 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -31,7 +31,7 @@ Arguments JMeq_refl {A x} , [A] x. Register JMeq as core.JMeq.type. Register JMeq_refl as core.JMeq.refl. -Hint Resolve JMeq_refl. +Hint Resolve JMeq_refl : core. Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. @@ -42,7 +42,7 @@ Proof. intros; destruct H; trivial. Qed. -Hint Immediate JMeq_sym. +Hint Immediate JMeq_sym : core. Register JMeq_sym as core.JMeq.sym. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index aec88f93bf..ac2a143472 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -305,13 +305,13 @@ Include MSetGenTree.Props X I. (** Automation and dedicated tactics *) -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 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. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree Ok : core. +Local Hint Constructors InT bst : core. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. +Local Hint Resolve elements_spec2 : core. (* Sometimes functional induction will expose too much of a tree structure. The following tactic allows factoring back @@ -496,7 +496,7 @@ Proof. specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L; [setoid_replace y with x|inv]; eauto. Qed. -Local Hint Resolve remove_min_gt_tree. +Local Hint Resolve remove_min_gt_tree : core. (** ** Merging two trees *) diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 95868861fa..888f9850c1 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -46,7 +46,7 @@ End InfoTyp. Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. -Hint Transparent elt. +Hint Transparent elt : core. Inductive tree : Type := | Leaf : tree @@ -342,11 +342,11 @@ 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 Immediate MX.eq_sym. -Local Hint Unfold In lt_tree gt_tree. -Local Hint Constructors InT bst. -Local Hint Unfold Ok. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree : core. +Local Hint Constructors InT bst : core. +Local Hint Unfold Ok : core. (** Automatic treatment of [Ok] hypothesis *) @@ -432,7 +432,7 @@ Lemma In_1 : Proof. induction s; simpl; intuition_in; eauto. Qed. -Local Hint Immediate In_1. +Local Hint Immediate In_1 : core. Instance In_compat : Proper (X.eq==>eq==>iff) InT. Proof. @@ -478,7 +478,7 @@ Proof. unfold gt_tree; intuition_in; order. Qed. -Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. Lemma lt_tree_not_in : forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t. @@ -516,7 +516,7 @@ Proof. intros x x' Hx s s' Hs H y Hy. subst. setoid_rewrite <- Hx; auto. Qed. -Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. Ltac induct s x := induction s as [|i l IHl x' r IHr]; simpl; intros; @@ -699,7 +699,7 @@ Proof. intros; unfold elements; apply elements_spec2'; auto. intros; inversion H0. Qed. -Local Hint Resolve elements_spec2. +Local Hint Resolve elements_spec2 : core. Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s). Proof. @@ -1035,7 +1035,7 @@ Qed. Definition Cmp c x y := CompSpec L.eq L.lt x y c. -Local Hint Unfold Cmp flip. +Local Hint Unfold Cmp flip : core. Lemma compare_end_Cmp : forall e2, Cmp (compare_end e2) nil (flatten_e e2). diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index f0e757157d..a4bbaef52d 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -884,10 +884,10 @@ Module MakeListOrdering (O:OrderedType). O.lt x y -> lt_list (x :: s) (y :: s') | lt_cons_eq : forall x y s s', O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s'). - Hint Constructors lt_list. + Hint Constructors lt_list : core. Definition lt := lt_list. - Hint Unfold lt. + Hint Unfold lt : core. Instance lt_strorder : StrictOrder lt. Proof. @@ -933,13 +933,13 @@ Module MakeListOrdering (O:OrderedType). left; MO.order. right; rewrite <- E12; auto. left; MO.order. right; rewrite E12; auto. Qed. - Hint Resolve eq_cons. + Hint Resolve eq_cons : core. Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 -> CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c. Proof. destruct c; simpl; inversion_clear 2; auto with relations. Qed. - Hint Resolve cons_CompSpec. + Hint Resolve cons_CompSpec : core. End MakeListOrdering. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 35fe4cee4e..7b64818b24 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -231,14 +231,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Notation In := (InA X.eq). Existing Instance X.eq_equiv. - Hint Extern 20 => solve [order]. + Hint Extern 20 => solve [order] : core. Definition IsOk s := Sort s. Class Ok (s:t) : Prop := ok : Sort s. - Hint Resolve ok. - Hint Unfold Ok. + Hint Resolve ok : core. + Hint Unfold Ok : core. Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }. @@ -276,7 +276,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. destruct H; constructor; tauto. Qed. - Hint Extern 1 (Ok _) => rewrite <- isok_iff. + Hint Extern 1 (Ok _) => rewrite <- isok_iff : core. Ltac inv_ok := match goal with | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok @@ -326,7 +326,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intuition. intros; elim_compare x a; inv; intuition. Qed. - Hint Resolve add_inf. + Hint Resolve add_inf : core. Global Instance add_ok s x : forall `(Ok s), Ok (add x s). Proof. @@ -353,7 +353,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto. Qed. - Hint Resolve remove_inf. + Hint Resolve remove_inf : core. Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s). Proof. @@ -396,7 +396,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction2. Qed. - Hint Resolve union_inf. + Hint Resolve union_inf : core. Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s'). Proof. @@ -422,7 +422,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. - Hint Resolve inter_inf. + Hint Resolve inter_inf : core. Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s'). Proof. @@ -452,7 +452,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. - Hint Resolve diff_inf. + Hint Resolve diff_inf : core. Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s'). Proof. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 3c7dea736b..29e57ff0a2 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -21,7 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose. +Hint Unfold transpose : core. (** First, a functor for Weak Sets in functorial version. *) @@ -735,7 +735,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). Proof. intros; rewrite cardinal_Empty; auto. Qed. - Hint Resolve cardinal_inv_1. + Hint Resolve cardinal_inv_1 : core. Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }. @@ -774,7 +774,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). exact Equal_cardinal. Qed. - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. (** ** Cardinal and set operators *) @@ -898,7 +898,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). auto with set. Qed. - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. End WPropertiesOn. @@ -922,7 +922,7 @@ Module OrdProperties (M:Sets). Import M.E. Import M. - Hint Resolve elements_spec2. + Hint Resolve elements_spec2 : core. Hint Immediate min_elt_spec1 min_elt_spec2 min_elt_spec3 max_elt_spec1 max_elt_spec2 max_elt_spec3 : set. @@ -961,7 +961,7 @@ Module OrdProperties (M:Sets). Proof. intros a b H; unfold leb. rewrite H; auto. Qed. - Hint Resolve gtb_compat leb_compat. + Hint Resolve gtb_compat leb_compat : core. Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index eab01a55b0..f9105fdf74 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -450,13 +450,13 @@ Include MSetGenTree.Props X Color. Local Notation Rd := (Node Red). 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 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. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree Ok : core. +Local Hint Constructors InT bst : core. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. +Local Hint Resolve elements_spec2 : core. (** ** Singleton set *) @@ -1136,7 +1136,7 @@ Record INV l1 l2 acc : Prop := { acc_sorted : sort X.lt acc; l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y; l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}. -Local Hint Resolve l1_sorted l2_sorted acc_sorted. +Local Hint Resolve l1_sorted l2_sorted acc_sorted : core. Lemma INV_init s1 s2 `(Ok s1, Ok s2) : INV (rev_elements s1) (rev_elements s2) nil. @@ -1506,8 +1506,8 @@ Class Rbt (t:tree) := RBT : exists d, rbt d t. (** ** Basic tactics and results about red-black *) Scheme rbt_ind := Induction for rbt Sort Prop. -Local Hint Constructors rbt rrt arbt. -Local Hint Extern 0 (notred _) => (exact I). +Local Hint Constructors rbt rrt arbt : core. +Local Hint Extern 0 (notred _) => (exact I) : core. Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction. Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end. Ltac nonzero n := destruct n as [|n]; [try split; invrb|]. @@ -1519,7 +1519,7 @@ Proof. destruct l, r; descolor; invrb; auto. Qed. -Local Hint Resolve rr_nrr_rb. +Local Hint Resolve rr_nrr_rb : core. Lemma arb_nrr_rb n t : arbt n t -> notredred t -> rbt n t. @@ -1533,7 +1533,7 @@ Proof. destruct 1; destruct t; descolor; invrb; auto. Qed. -Local Hint Resolve arb_nrr_rb arb_nr_rb. +Local Hint Resolve arb_nrr_rb arb_nr_rb : core. (** ** A Red-Black tree has indeed a logarithmic depth *) diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 8df1ff1cdb..19058a767e 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -123,15 +123,15 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. 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. + Hint Resolve eqr eqtrans : core. + Hint Immediate eqsym : core. Definition IsOk := NoDup. Class Ok (s:t) : Prop := ok : NoDup s. - Hint Unfold Ok. - Hint Resolve ok. + Hint Unfold Ok : core. + Hint Resolve ok : core. Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 784e81758c..4bcd22543f 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -60,7 +60,7 @@ Section ZModulo. apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. - Hint Resolve wB_pos. + Hint Resolve wB_pos : core. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. Proof. @@ -71,7 +71,7 @@ Section ZModulo. Proof. unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. - Hint Resolve spec_to_Z_1 spec_to_Z_2. + Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. Proof. @@ -732,7 +732,7 @@ Section ZModulo. Proof. induction p; simpl; auto with zarith. Qed. - Hint Resolve Ptail_pos. + Hint Resolve Ptail_pos : core. Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. Proof. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8e1be0d702..4539dea276 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -383,7 +383,7 @@ f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed. -Hint Resolve log_good_step. +Hint Resolve log_good_step : core. Theorem log_init : forall n, n < 2 -> log n == 0. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index c2316689fc..d86112abc0 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -26,7 +26,7 @@ Arguments id {A} x. Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x). -Hint Unfold compose. +Hint Unfold compose : core. Declare Scope program_scope. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 8479b9a2bb..f9d23e3cf6 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -110,7 +110,7 @@ Section Measure_well_founded. End Measure_well_founded. -Hint Resolve measure_wf. +Hint Resolve measure_wf : core. Section Fix_rects. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 81c318138e..f18fca99a0 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -66,7 +66,7 @@ Proof. rewrite hq, hq' in H'. subst q'. f_equal. apply eq_proofs_unicity. intros. repeat decide equality. Qed. -Hint Resolve Qc_is_canon. +Hint Resolve Qc_is_canon : core. Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'. Proof. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index c832962590..b4c869b4dd 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -21,7 +21,7 @@ intros. now apply not_O_IZR. Qed. -Hint Resolve IZR_nz Rmult_integral_contrapositive. +Hint Resolve IZR_nz Rmult_integral_contrapositive : core. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. Proof. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 59a1049654..ec283b886e 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1087,7 +1087,7 @@ Proof. replace (r2 + r1 + - r2) with r1 by ring. exact H. Qed. -Hint Resolve Ropp_gt_lt_contravar. +Hint Resolve Ropp_gt_lt_contravar : core. Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. @@ -1204,7 +1204,7 @@ Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. -Hint Resolve Rmult_lt_compat_r. +Hint Resolve Rmult_lt_compat_r : core. Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. Proof. eauto using Rmult_lt_compat_r with rorders. Qed. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 3977097e8c..61fe55770b 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -95,7 +95,7 @@ End Bounds. Hint Resolve Totally_ordered_definition Upper_Bound_definition Lower_Bound_definition Lub_definition Glb_definition Bottom_definition Definition_of_Complete Definition_of_Complete - Definition_of_Conditionally_complete. + Definition_of_Conditionally_complete : core. Section Specific_orders. Variable U : Type. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index bdeeb6a7c7..a0271a88a3 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -46,7 +46,7 @@ Section Approx. Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X. End Approx. -Hint Resolve Defn_of_Approximant. +Hint Resolve Defn_of_Approximant : core. Section Infinite_sets. Variable U : Type. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 88bcd6555c..50a7e401f8 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -38,43 +38,43 @@ Variable U : Type. Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := Definition_of_Power_set : forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X. -Hint Resolve Definition_of_Power_set. +Hint Resolve Definition_of_Power_set : core. Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. intro X; red. intros x H'; elim H'. Qed. -Hint Resolve Empty_set_minimal. +Hint Resolve Empty_set_minimal : core. Theorem Power_set_Inhabited : forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X). intro X. apply Inhabited_intro with (Empty_set U); auto with sets. Qed. -Hint Resolve Power_set_Inhabited. +Hint Resolve Power_set_Inhabited : core. Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U). auto 6 with sets. Qed. -Hint Resolve Inclusion_is_an_order. +Hint Resolve Inclusion_is_an_order : core. Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U). elim Inclusion_is_an_order; auto with sets. Qed. -Hint Resolve Inclusion_is_transitive. +Hint Resolve Inclusion_is_transitive : core. Definition Power_set_PO : Ensemble U -> PO (Ensemble U). intro A; try assumption. apply Definition_of_PO with (Power_set A) (Included U); auto with sets. Defined. -Hint Unfold Power_set_PO. +Hint Unfold Power_set_PO : core. Theorem Strict_Rel_is_Strict_Included : same_relation (Ensemble U) (Strict_Included U) (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))). auto with sets. Qed. -Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. +Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core. Lemma Strict_inclusion_is_transitive_with_inclusion : forall x y z:Ensemble U, @@ -109,7 +109,7 @@ Theorem Empty_set_is_Bottom : forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). intro A; apply Bottom_definition; simpl; auto with sets. Qed. -Hint Resolve Empty_set_is_Bottom. +Hint Resolve Empty_set_is_Bottom : core. Theorem Union_minimal : forall a b X:Ensemble U, @@ -117,7 +117,7 @@ Theorem Union_minimal : intros a b X H' H'0; red. intros x H'1; elim H'1; auto with sets. Qed. -Hint Resolve Union_minimal. +Hint Resolve Union_minimal : core. Theorem Intersection_maximal : forall a b X:Ensemble U, @@ -145,7 +145,7 @@ intros a b; red. intros x H'; elim H'; auto with sets. Qed. Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l - Intersection_decreases_r. + Intersection_decreases_r : core. Theorem Union_is_Lub : forall A a b:Ensemble U, diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 296ec42add..d275487e15 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -52,7 +52,7 @@ intros x y z h; elim h; intros H'3 H'4; clear h. intro h; elim h; intros H'5 H'6; clear h. split; apply H'1 with y; auto 10 with sets. Qed. -Hint Resolve Equiv_from_preorder. +Hint Resolve Equiv_from_preorder : core. Theorem Equiv_from_order : forall (U:Type) (R:Relation U), @@ -60,21 +60,21 @@ Theorem Equiv_from_order : Proof. intros U R H'; elim H'; auto 10 with sets. Qed. -Hint Resolve Equiv_from_order. +Hint Resolve Equiv_from_order : core. Theorem contains_is_preorder : forall U:Type, Preorder (Relation U) (contains U). Proof. auto 10 with sets. Qed. -Hint Resolve contains_is_preorder. +Hint Resolve contains_is_preorder : core. Theorem same_relation_is_equivalence : forall U:Type, Equivalence (Relation U) (same_relation U). Proof. unfold same_relation at 1; auto 10 with sets. Qed. -Hint Resolve same_relation_is_equivalence. +Hint Resolve same_relation_is_equivalence : core. Theorem cong_reflexive_same_relation : forall (U:Type) (R R':Relation U), diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 0c1f670d0e..18ea019526 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -38,7 +38,7 @@ Proof. intros U R x y H'; red. exists y; auto with sets. Qed. -Hint Resolve Rstar_imp_coherent. +Hint Resolve Rstar_imp_coherent : core. Theorem coherent_symmetric : forall (U:Type) (R:Relation U), Symmetric U (coherent U R). diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 7940bda1a7..0ff304ed6b 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -41,21 +41,21 @@ Definition Singleton (a:A) := end). Definition In (s:uniset) (a:A) : Prop := charac s a = true. -Hint Unfold In. +Hint Unfold In : core. (** uniset inclusion *) Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). -Hint Unfold incl. +Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. -Hint Unfold seq. +Hint Unfold seq : core. Lemma leb_refl : forall b:bool, leb b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl. +Hint Resolve leb_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. @@ -71,7 +71,7 @@ Lemma seq_refl : forall x:uniset, seq x x. Proof. destruct x; unfold seq; auto. Qed. -Hint Resolve seq_refl. +Hint Resolve seq_refl : core. Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. Proof. @@ -94,21 +94,21 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. unfold seq; unfold union; simpl; auto. Qed. -Hint Resolve union_empty_left. +Hint Resolve union_empty_left : core. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). Proof. unfold seq; unfold union; simpl. intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. -Hint Resolve union_empty_right. +Hint Resolve union_empty_right : core. Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). Proof. unfold seq; unfold charac; unfold union. destruct x; destruct y; auto with bool. Qed. -Hint Resolve union_comm. +Hint Resolve union_comm : core. Lemma union_ass : forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). @@ -116,7 +116,7 @@ Proof. unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed. -Hint Resolve union_ass. +Hint Resolve union_ass : core. Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). Proof. @@ -124,7 +124,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. -Hint Resolve seq_left. +Hint Resolve seq_left : core. Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). Proof. @@ -132,7 +132,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. -Hint Resolve seq_right. +Hint Resolve seq_right : core. (** All the proofs that follow duplicate [Multiset_of_A] *) diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 2ef162be4e..6a22501afa 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -36,8 +36,8 @@ Section defs. Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. - Hint Resolve leA_refl. - Hint Immediate eqA_dec leA_dec leA_antisym. + Hint Resolve leA_refl : core. + Hint Immediate eqA_dec leA_dec leA_antisym : core. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 7b99b3626f..f5bc9eee4e 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -31,7 +31,7 @@ Inductive Permutation : list A -> list A -> Prop := | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''. -Local Hint Constructors Permutation. +Local Hint Constructors Permutation : core. (** Some facts about [Permutation] *) @@ -71,13 +71,13 @@ Qed. End Permutation. -Hint Resolve Permutation_refl perm_nil perm_skip. +Hint Resolve Permutation_refl perm_nil perm_skip : core. (* These hints do not reduce the size of the problem to solve and they must be used with care to avoid combinatoric explosions *) -Local Hint Resolve perm_swap perm_trans. -Local Hint Resolve Permutation_sym Permutation_trans. +Local Hint Resolve perm_swap perm_trans : core. +Local Hint Resolve Permutation_sym Permutation_trans : core. (* This provides reflexivity, symmetry and transitivity and rewriting on morphims to come *) @@ -156,7 +156,7 @@ Qed. Lemma Permutation_cons_append : forall (l : list A) x, Permutation (x :: l) (l ++ x :: nil). Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed. -Local Hint Resolve Permutation_cons_append. +Local Hint Resolve Permutation_cons_append : core. Theorem Permutation_app_comm : forall (l l' : list A), Permutation (l ++ l') (l' ++ l). @@ -166,7 +166,7 @@ Proof. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed. -Local Hint Resolve Permutation_app_comm. +Local Hint Resolve Permutation_app_comm : core. Theorem Permutation_cons_app : forall (l l1 l2:list A) a, Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2). @@ -175,7 +175,7 @@ Proof. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed. -Local Hint Resolve Permutation_cons_app. +Local Hint Resolve Permutation_cons_app : core. Lemma Permutation_Add a l l' : Add a l l' -> Permutation (a::l) l'. Proof. @@ -188,7 +188,7 @@ Theorem Permutation_middle : forall (l1 l2:list A) a, Proof. auto. Qed. -Local Hint Resolve Permutation_middle. +Local Hint Resolve Permutation_middle : core. Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). Proof. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 89e9c7f3e1..6782dd9ca3 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -137,8 +137,8 @@ Section defs. End defs. -Hint Constructors HdRel. -Hint Constructors Sorted. +Hint Constructors HdRel : core. +Hint Constructors Sorted : core. (* begin hide *) (* Compatibility with deprecated file Sorting.v *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 24333ad815..f82ca5fa3c 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -38,8 +38,8 @@ Module KeyDecidableType(D:DecidableType). Definition eqke (p p':key*elt) := eq (fst p) (fst p') /\ (snd p) = (snd p'). - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold eqk eqke : core. + Hint Extern 2 (eqke ?a ?b) => split : core. (* eqke is stricter than eqk *) @@ -70,8 +70,8 @@ Module KeyDecidableType(D:DecidableType). unfold eqke; intuition; [ eauto | congruence ]. Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Immediate eqk_sym eqke_sym : core. Global Instance eqk_equiv : Equivalence eqk. Proof. split; eauto. Qed. @@ -84,7 +84,7 @@ Module KeyDecidableType(D:DecidableType). Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. @@ -94,7 +94,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -140,13 +140,13 @@ Module KeyDecidableType(D:DecidableType). End Elt. - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Resolve In_inv_2 In_inv_3. + Hint Unfold eqk eqke : core. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve InA_eqke_eqk : core. + Hint Unfold MapsTo In : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 5f60a979c6..4143dba547 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -53,8 +53,8 @@ Module Type IsEqOrig (Import E:Eq'). Axiom eq_refl : forall x : t, x==x. Axiom eq_sym : forall x y : t, x==y -> y==x. Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z. - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. + Hint Immediate eq_sym : core. + Hint Resolve eq_refl eq_trans : core. End IsEqOrig. (** * Types with decidable equality *) diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 7b6ee2eaca..c738b57f44 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -22,7 +22,7 @@ Module KeyDecidableType(D:DecidableType). Definition eqk {elt} : relation (key*elt) := D.eq @@1. Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq. - Hint Unfold eqk eqke. + Hint Unfold eqk eqke : core. (** eqk, eqke are equalities *) @@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType). Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. Proof. trivial. Qed. - Hint Resolve eqke_1 eqke_2 eqk_1. + Hint Resolve eqke_1 eqke_2 eqk_1 : core. (* Additional facts *) @@ -69,7 +69,7 @@ Module KeyDecidableType(D:DecidableType). Proof. induction 1; firstorder. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : InA eqk p m -> exists q, eqk p q /\ InA eqke q m. @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). Definition In {elt} k m := exists e:elt, MapsTo k e m. - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* Alternative formulations for [In k l] *) @@ -167,9 +167,9 @@ Module KeyDecidableType(D:DecidableType). eauto with *. Qed. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve InA_eqke_eqk. - Hint Resolve In_inv_2 In_inv_3. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve InA_eqke_eqk : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index f6fc247d5a..d000b75bf4 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -42,8 +42,8 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + Hint Immediate eq_sym : core. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. End MiniOrderedType. @@ -143,9 +143,9 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. - Hint Resolve gt_not_eq eq_not_lt. - Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq. - Hint Resolve eq_not_gt lt_antirefl lt_not_gt. + Hint Resolve gt_not_eq eq_not_lt : core. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core. + Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core. Lemma elim_compare_eq : forall x y : t, @@ -247,8 +247,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. +Hint Immediate In_eq Inf_lt : core. End OrderedTypeFacts. @@ -266,8 +266,8 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold eqk eqke ltk : core. + Hint Extern 2 (eqke ?a ?b) => split : core. (* eqke is stricter than eqk *) @@ -283,7 +283,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l. + Hint Immediate ltk_right_r ltk_right_l : core. (* eqk, eqke are equalities, ltk is a strict order *) @@ -319,9 +319,9 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. + Hint Immediate eqk_sym eqke_sym : core. Global Instance eqk_equiv : Equivalence eqk. Proof. constructor; eauto. Qed. @@ -359,22 +359,22 @@ Module KeyOrderedType(O:OrderedType). intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; eauto. Qed. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. + Hint Resolve eqk_not_ltk : core. + Hint Immediate ltk_eqk eqk_ltk : core. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -405,8 +405,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -469,19 +469,19 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. - Hint Resolve In_inv_2 In_inv_3. + Hint Unfold eqk eqke ltk : core. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. + Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve eqk_not_ltk : core. + Hint Immediate ltk_eqk eqk_ltk : core. + Hint Resolve InA_eqke_eqk : core. + Hint Unfold MapsTo In : core. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. + Hint Resolve Sort_Inf_NotIn : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyOrderedType. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 42756ad339..310a22a0a4 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -181,7 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder we coerce [bool] into [Prop]. *) Local Coercion is_true : bool >-> Sortclass. -Hint Unfold is_true. +Hint Unfold is_true : core. Module Type HasLeb (Import T:Typ). Parameter Inline leb : t -> t -> bool. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index abdb9eff05..fef9b14a9e 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -50,8 +50,8 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed. -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. +Hint Immediate In_eq Inf_lt : core. End OrderedTypeLists. @@ -66,7 +66,7 @@ Module KeyOrderedType(O:OrderedType). Definition ltk {elt} : relation (key*elt) := O.lt @@1. - Hint Unfold ltk. + Hint Unfold ltk : core. (* ltk is a strict order *) @@ -109,8 +109,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l. Proof. apply InfA_ltA; auto with *. Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p. Proof. apply SortA_InfA_InA; auto with *. Qed. @@ -148,10 +148,10 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Resolve ltk_not_eqk ltk_not_eqke. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. + Hint Resolve ltk_not_eqk ltk_not_eqke : core. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. + Hint Resolve Sort_Inf_NotIn : core. End KeyOrderedType. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 4a2bddf35c..7f96aa6b87 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -269,28 +269,28 @@ Section SCANNING. Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := |Forall_nil: Forall P [] |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v). -Hint Constructors Forall. +Hint Constructors Forall : core. Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop := |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v) |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v). -Hint Constructors Exists. +Hint Constructors Exists : core. Inductive In {A} (a:A): forall {n}, t A n -> Prop := |In_cons_hd {m} (v: t A m): In a (a::v) |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v). -Hint Constructors In. +Hint Constructors In : core. Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Forall2_nil: Forall2 P [] [] |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 -> Forall2 P (x1::v1) (x2::v2). -Hint Constructors Forall2. +Hint Constructors Forall2 : core. Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2) |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2). -Hint Constructors Exists2. +Hint Constructors Exists2 : core. End SCANNING. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index ff233ef9c6..18c4bedd9a 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -22,7 +22,7 @@ Section WfInclusion. apply Acc_intro; auto with sets. Qed. - Hint Resolve Acc_incl. + Hint Resolve Acc_incl : core. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. Proof. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 59068623ae..0d56d88869 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,7 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. - Hint Resolve Acc_clos_trans. + Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. Proof. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 74614e114a..c278cada61 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -73,7 +73,7 @@ Proof. intros; unfold Remainder, Remainder_alt; omega with *. Qed. -Hint Unfold Remainder. +Hint Unfold Remainder : core. (** Now comes the fully general result about Euclidean division. *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 24412e9431..b8c7319939 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -47,7 +47,7 @@ Section Log_pos. (* Log of positive integers *) | xI n => Z.succ (Z.succ (log_inf n)) (* 2n+1 *) end. - Hint Unfold log_inf log_sup. + Hint Unfold log_inf log_sup : core. Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). Proof. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1fab35b650..59aa364223 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1066,13 +1066,28 @@ let vernac_restore_state file = let vernac_create_hintdb ~module_local id b = Hints.create_hint_db module_local id full_transparent_state b -let vernac_remove_hints ~module_local dbs ids = - Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids) +let warn_implicit_core_hint_db = + CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated" + (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " + ++ strbrk"Please specify a hint database.") + +let vernac_remove_hints ~module_local dbnames ids = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in + Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids) -let vernac_hints ~atts lb h = +let vernac_hints ~atts dbnames h = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local lb (Hints.interp_hints poly h) + Hints.add_hints ~local dbnames (Hints.interp_hints poly h) let vernac_syntactic_definition ~module_local lid x y = Dumpglob.dump_definition lid false "syndef"; |