Merge pull request #27 from coq-community/export-hint

change from global to export locality for hints
coq-community · Jul 30, 2021 · 17d3b8d · 17d3b8d
2 parents 9188dec + 94dee33
commit 17d3b8d
Show file tree

Hide file tree

Showing 13 changed files with 27 additions and 27 deletions.
diff --git a/theories/AuxLib.v b/theories/AuxLib.v
@@ -77,7 +77,7 @@ rewrite <- le_plus_minus; auto.
 Qed.
 
 End Minus.
-Global Hint Resolve le_minus: arith.
+#[export] Hint Resolve le_minus: arith.
 
 (*A function to compare naturals *)
 Section LeBool.

diff --git a/theories/BTree.v b/theories/BTree.v
@@ -409,6 +409,6 @@ Arguments distinct_leaves [A].
 Arguments compute_code [A].
 Arguments number_of_nodes [A].
 
-Global Hint Constructors inb : core.
-Global Hint Resolve distinct_leaves_leaf : core.
-Global Hint Resolve length_compute_lt_O : core.
+#[export] Hint Constructors inb : core.
+#[export] Hint Resolve distinct_leaves_leaf : core.
+#[export] Hint Resolve length_compute_lt_O : core.
diff --git a/theories/Code.v b/theories/Code.v
@@ -638,9 +638,9 @@ Arguments find_val [A].
 Arguments in_alphabet [A].
 Arguments unique_prefix [A].
 Arguments not_null [A].
-Global Hint Constructors is_prefix : core.
-Global Hint Resolve is_prefix_refl : core.
-Global Hint Resolve not_null_map : core.
-Global Hint Resolve unique_prefix_nil : core.
-Global Hint Resolve in_alphabet_nil in_alphabet_cons : core.
-Global Hint Resolve not_null_app : core.
+#[export] Hint Constructors is_prefix : core.
+#[export] Hint Resolve is_prefix_refl : core.
+#[export] Hint Resolve not_null_map : core.
+#[export] Hint Resolve unique_prefix_nil : core.
+#[export] Hint Resolve in_alphabet_nil in_alphabet_cons : core.
+#[export] Hint Resolve not_null_app : core.
diff --git a/theories/Cover.v b/theories/Cover.v
@@ -348,4 +348,4 @@ Qed.
 
 End Cover.
 Arguments cover [A].
-Global Hint Constructors cover : core.
+#[export] Hint Constructors cover : core.
diff --git a/theories/CoverMin.v b/theories/CoverMin.v
@@ -87,4 +87,4 @@ Qed.
 
 End CoverMin.
 
-Global Hint Resolve cover_min_one : core.
+#[export] Hint Resolve cover_min_one : core.
diff --git a/theories/Frequency.v b/theories/Frequency.v
@@ -316,5 +316,5 @@ Arguments add_frequency_list [A].
 Arguments frequency_list [A].
 Arguments number_of_occurrences [A].
 
-Global Hint Resolve in_frequency_map : core.
-Global Hint Resolve frequency_list_unique : core.
+#[export] Hint Resolve in_frequency_map : core.
+#[export] Hint Resolve frequency_list_unique : core.
diff --git a/theories/HeightPred.v b/theories/HeightPred.v
@@ -499,4 +499,4 @@ Qed.
 
 End HeightPred.
 Arguments height_pred [A].
-Global Hint Resolve height_pred_nil height_pred_node : core.
+#[export] Hint Resolve height_pred_nil height_pred_node : core.
diff --git a/theories/Ordered.v b/theories/Ordered.v
@@ -127,7 +127,7 @@ Qed.
 
 End ordered.
 
-Global Hint Constructors ordered : core.
+#[export] Hint Constructors ordered : core.
 
 Arguments ordered [A].
 

diff --git a/theories/OrderedCover.v b/theories/OrderedCover.v
@@ -134,4 +134,4 @@ Qed.
 
 End OrderedCover.
 Arguments ordered_cover [A].
-Global Hint Resolve ordered_cover_one ordered_cover_node : core.
+#[export] Hint Resolve ordered_cover_one ordered_cover_node : core.
diff --git a/theories/PBTree.v b/theories/PBTree.v
@@ -1239,9 +1239,9 @@ Arguments distinct_pbleaves [A].
 Arguments compute_pbcode [A].
 Arguments inpb_dec [A].
 
-Global Hint Constructors inpb : core.
-Global Hint Resolve distinct_pbleaves_pbleaf : core.
-Global Hint Resolve distinct_pbleaves_pbleft distinct_pbleaves_pbright : core.
-Global Hint Resolve compute_pbcode_not_null : core.
-Global Hint Resolve compute_pbcode_not_null : core.
-Global Hint Constructors pbfree : core.
+#[export] Hint Constructors inpb : core.
+#[export] Hint Resolve distinct_pbleaves_pbleaf : core.
+#[export] Hint Resolve distinct_pbleaves_pbleft distinct_pbleaves_pbright : core.
+#[export] Hint Resolve compute_pbcode_not_null : core.
+#[export] Hint Resolve compute_pbcode_not_null : core.
+#[export] Hint Constructors pbfree : core.
diff --git a/theories/SubstPred.v b/theories/SubstPred.v
@@ -116,4 +116,4 @@ Qed.
 
 End SubstPred.
 Arguments subst_pred [A].
-Global Hint Resolve subst_pred_id : core.
+#[export] Hint Resolve subst_pred_id : core.
diff --git a/theories/UList.v b/theories/UList.v
@@ -122,4 +122,4 @@ End UniqueList.
 
 Arguments ulist [A].
 
-Global Hint Constructors ulist : core.
+#[export] Hint Constructors ulist : core.
diff --git a/theories/UniqueKey.v b/theories/UniqueKey.v
@@ -137,7 +137,7 @@ apply H; apply ulist_inv with (1 := H0); auto.
 Qed. 
 
 End UniqueKey.
-Global Hint Constructors unique_key : core.
+#[export] Hint Constructors unique_key : core.
 Arguments unique_key [A B].
 
 (* Uniqueness is compatible with map for injective functions *)
@@ -161,4 +161,4 @@ apply H4.
 intros b2; red in |- *; intros H7.
 case (H5 b2); auto.
 Qed.
-Global Hint Resolve unique_key_app unique_key_map : core.
+#[export] Hint Resolve unique_key_app unique_key_map : core.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -87,4 +87,4 @@ Qed.

		End CoverMin.

		Global Hint Resolve cover_min_one : core.
		#[export] Hint Resolve cover_min_one : core.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -122,4 +122,4 @@ End UniqueList.

		Arguments ulist [A].

		Global Hint Constructors ulist : core.
		#[export] Hint Constructors ulist : core.