Adapt w.r.t. coq/coq#16004.

uwplse · Jun 28, 2022 · 22f7f5a · 22f7f5a
1 parent 064cc4f
commit 22f7f5a
Show file tree

Hide file tree

Showing 9 changed files with 20 additions and 0 deletions.
diff --git a/core/LabeledNet.v b/core/LabeledNet.v
@@ -531,4 +531,5 @@ Section LabeledStepOrderDynamicFailure.
   Qed.
 End LabeledStepOrderDynamicFailure.
 
+#[global]
 Hint Extern 4 (@LabeledMultiParams _) => apply unlabeled_multi_params : typeclass_instances.
diff --git a/core/VerdiHints.v b/core/VerdiHints.v
@@ -1,4 +1,6 @@
 Require Import StructTact.Util.
 
+#[global]
 Hint Resolve app_cons_in : core.
+#[global]
 Hint Resolve app_cons_in_rest : core.
diff --git a/lib/FMapVeryWeak.v b/lib/FMapVeryWeak.v
@@ -20,6 +20,7 @@ Module Type VWS.
   Declare Module E : DecidableType.
 
   Definition key := E.t.
+#[global]
   Hint Transparent key : core.
 
   Parameter t : Type -> Type.

diff --git a/systems/Counter.v b/systems/Counter.v
@@ -62,6 +62,7 @@ Definition InputHandler (me : Name) (i : Input) : Handler Data :=
   | backup => BackupInputHandler i
   end.
 
+#[global]
 Instance Counter_BaseParams : BaseParams :=
   {
     data := Data;
@@ -81,6 +82,7 @@ Proof.
   repeat constructor; simpl; intuition discriminate.
 Qed.
 
+#[global]
 Instance Counter_MultiParams : MultiParams Counter_BaseParams :=
   {
     name := Name;

diff --git a/systems/Log.v b/systems/Log.v
@@ -111,6 +111,9 @@ Section Log.
     { do_reboot := do_log_reboot }.
 End Log.
 
+#[global]
 Hint Extern 5 (@BaseParams) => apply log_base_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@DiskOpMultiParams _) => apply log_multi_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@DiskOpFailureParams _ _) => apply log_failure_params : typeclass_instances.
diff --git a/systems/SeqNum.v b/systems/SeqNum.v
@@ -69,5 +69,7 @@ Section SeqNum.
     }.
 End SeqNum.
 
+#[global]
 Hint Extern 5 (@BaseParams) => apply base_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@MultiParams _) => apply multi_params : typeclass_instances.
diff --git a/systems/SerializedMsgParams.v b/systems/SerializedMsgParams.v
@@ -68,9 +68,15 @@ Section Serialized.
     }.
 End Serialized.
 
+#[global]
 Hint Extern 5 (@BaseParams) => apply serialized_base_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@MultiParams _) => apply serialized_multi_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@FailureParams _ _) => apply serialized_failure_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@NameOverlayParams _ _) => apply serialized_name_overlay_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@FailMsgParams _ _) => apply serialized_fail_msg_params : typeclass_instances.
+#[global]
 Hint Extern 5 (@NewMsgParams _ _) => apply serialized_new_msg_params : typeclass_instances.
diff --git a/systems/VarD.v b/systems/VarD.v
@@ -87,13 +87,15 @@ Definition VarDHandler := runHandler VarDHandler'.
 
 Definition init_map := Map.empty string.
 
+#[global]
 Instance vard_base_params : BaseParams :=
   {
     data := data ;
     input := input ;
     output := output
   }.
 
+#[global]
 Instance vard_one_node_params : OneNodeParams _ :=
   {
     init := init_map ;

diff --git a/systems/VarDPrimaryBackup.v b/systems/VarDPrimaryBackup.v
@@ -7,6 +7,7 @@ Require Import Verdi.PrimaryBackup.
 
 Open Scope string_scope.
 
+#[global]
 Instance vard_pbj_params : PrimaryBackupParams vard_base_params :=
   {
     input_eq_dec := VarD.input_eq_dec