From 666d14e91d41f0f952d5c5c65391f152c6a71025 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 24 Sep 2024 08:49:20 +0200 Subject: [PATCH] add #[export] to all Hints --- coq/metatheory/Environment.v | 12 ++++++------ coq/metatheory/Metatheory.v | 6 +++--- coq/terms/equiv.v | 10 +++++----- coq/typing/morph.v | 2 +- coq/typing/subtype.v | 6 +++--- coq/typing/typing.v | 2 +- 6 files changed, 19 insertions(+), 19 deletions(-) diff --git a/coq/metatheory/Environment.v b/coq/metatheory/Environment.v index 8876659..16606b9 100644 --- a/coq/metatheory/Environment.v +++ b/coq/metatheory/Environment.v @@ -269,7 +269,7 @@ Proof. simpl. intros. fsetdec. Qed. -Hint Rewrite +#[export] Hint Rewrite cons_concat map_singleton_list dom_singleton_list concat_nil nil_concat concat_assoc map_nil map_single map_push map_concat @@ -329,7 +329,7 @@ Tactic Notation "rewrite_env" constr(E) "in" hyp(H) := (** ** Hints *) -Hint Constructors ok. +#[export] Hint Constructors ok. Local Hint Extern 1 (~ In _ _) => simpl_env in *; fsetdec. @@ -498,9 +498,9 @@ End BindsProperties. (** ** Hints *) -Hint Immediate ok_remove_mid ok_remove_mid_cons. +#[export] Hint Immediate ok_remove_mid ok_remove_mid_cons. -Hint Resolve +#[export] Hint Resolve ok_push ok_singleton ok_map ok_map_app_l binds_singleton binds_head binds_tail. @@ -655,6 +655,6 @@ End AdditionalBindsProperties. (* *********************************************************************** *) (** * ## Automation and tactics (III) *) -Hint Resolve binds_map binds_concat_ok binds_weaken binds_weaken_at_head. +#[export] Hint Resolve binds_map binds_concat_ok binds_weaken binds_weaken_at_head. -Hint Immediate binds_remove_mid binds_remove_mid_cons. +#[export] Hint Immediate binds_remove_mid binds_remove_mid_cons. diff --git a/coq/metatheory/Metatheory.v b/coq/metatheory/Metatheory.v index e8158c7..266dba1 100644 --- a/coq/metatheory/Metatheory.v +++ b/coq/metatheory/Metatheory.v @@ -94,7 +94,7 @@ Tactic Notation particular those arising from cofinite quantification. *) Create HintDb MetatheoryHints. -Hint Resolve notin_empty notin_singleton notin_union :MetatheoryHints. +#[export] Hint Resolve notin_empty notin_singleton notin_union :MetatheoryHints. (*Hint Extern 4 (_ `notin` _) => simpl_env; notin_solve :MetatheoryHints. -Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve :MetatheoryHints. -*) \ No newline at end of file +#[export] Hint Extern 4 (_ <> _ :> atom) => simpl_env; notin_solve :MetatheoryHints. +*) diff --git a/coq/terms/equiv.v b/coq/terms/equiv.v index c22e804..5bed5ff 100644 --- a/coq/terms/equiv.v +++ b/coq/terms/equiv.v @@ -40,7 +40,7 @@ Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop := where "S '-->distribute-ladder' T" := (type_distribute_ladder S T). -Hint Constructors type_distribute_ladder : type_eq_hints. +#[export] Hint Constructors type_distribute_ladder : type_eq_hints. Reserved Notation "S '-->condense-ladder' T" (at level 40). Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop := @@ -76,7 +76,7 @@ Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop := where "S '-->condense-ladder' T" := (type_condense_ladder S T). -Hint Constructors type_condense_ladder : type_eq_hints. +#[export] Hint Constructors type_condense_ladder : type_eq_hints. (** Inversion Lemma: `-->distribute-ladder` is the inverse of `-->condense-ladder @@ -104,8 +104,8 @@ Proof. all: auto with type_eq_hints. Qed. -Hint Resolve condense_inverse :type_eq_hints. -Hint Resolve distribute_inverse :type_eq_hints. +#[export] Hint Resolve condense_inverse :type_eq_hints. +#[export] Hint Resolve distribute_inverse :type_eq_hints. (** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *) @@ -149,7 +149,7 @@ Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop := where "S '===' T" := (type_eq S T). -Hint Constructors type_eq : type_eq_hints. +#[export] Hint Constructors type_eq : type_eq_hints. (** Symmetry of === *) Lemma TEq_Symm : diff --git a/coq/typing/morph.v b/coq/typing/morph.v index b7dd49a..4c9e3e7 100644 --- a/coq/typing/morph.v +++ b/coq/typing/morph.v @@ -40,7 +40,7 @@ Inductive morphism_path : env -> type_DeBruijn -> type_DeBruijn -> Prop := where "Γ '|-' s '~~>' t" := (morphism_path Γ s t). Create HintDb morph_path_hints. -Hint Constructors morphism_path :morph_path_hints. +#[export] Hint Constructors morphism_path :morph_path_hints. Lemma id_morphism_path : forall Γ τ, type_lc τ -> diff --git a/coq/typing/subtype.v b/coq/typing/subtype.v index 18d9679..bc7b79b 100644 --- a/coq/typing/subtype.v +++ b/coq/typing/subtype.v @@ -35,9 +35,9 @@ Inductive is_conv_subtype : type_DeBruijn -> type_DeBruijn -> Prop := | TSubConv_Morph : forall x y y', [< x ~ y >] ~<= [< x ~ y' >] where "s '~<=' t" := (is_conv_subtype s t). -Hint Constructors is_repr_subtype :subtype_hints. -Hint Constructors is_conv_subtype :subtype_hints. -Hint Constructors type_eq :subtype_hints. +#[export] Hint Constructors is_repr_subtype :subtype_hints. +#[export] Hint Constructors is_conv_subtype :subtype_hints. +#[export] Hint Constructors type_eq :subtype_hints. (* Every Representational Subtype is a Convertible Subtype *) diff --git a/coq/typing/typing.v b/coq/typing/typing.v index ec19fe0..1ed0d16 100644 --- a/coq/typing/typing.v +++ b/coq/typing/typing.v @@ -70,7 +70,7 @@ where "Γ '|-' x '\is' τ" := (typing Γ x τ). Create HintDb typing_hints. -Hint Constructors typing :typing_hints. +#[export] Hint Constructors typing :typing_hints. Reserved Notation "Γ '|-' '[[' e \is τ ']]' '=' f" (at level 101).