Adapt w.r.t. coq/coq#18895. (#110)

mit-plv · Apr 10, 2024 · ebd7475 · ebd7475
1 parent 9aaab98
commit ebd7475
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 6 deletions.
diff --git a/src/Common/MSetExtensions.v b/src/Common/MSetExtensions.v
@@ -107,7 +107,7 @@ Module MSetExtensionsOn (E: DecidableType) (Import M: WSetsOn E).
   Create HintDb sets discriminated.
   Create HintDb setsb discriminated.
   Global Hint Immediate union_subset_1 union_subset_2 inter_subset_1 inter_subset_2 equal_refl : sets.
-  Global Hint Resolve (BasicFacts.inter_s_m : forall x y _ x' y' _, _) : sets.
+  Global Hint Extern 2 => simple apply (BasicFacts.inter_s_m : forall x y _ x' y' _, _) : sets.
 
   Ltac simplify_sets_step :=
     idtac;

diff --git a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v
@@ -23,7 +23,7 @@ Section fold_correctness.
           (prerelated : Ensemble String -> T -> Prop)
           {aicdata : AbstractInterpretationCorrectness prerelated}.
   Context (G : pregrammar' Char).
-  Local Hint Immediate (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
+  Local Hint Extern 1 (opt.compile_item_data _ _) => simple apply (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
   Context (compiled_productions : list (opt.productions state))
           (Hcompiled_productions : List.map opt.compile_productions (List.map snd (pregrammar_productions G)) = compiled_productions).
 

diff --git a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v
@@ -446,7 +446,7 @@ Section fold_correctness.
     }.
 
   Context {aicdata : AbstractInterpretationCorrectness}.
-  Local Hint Immediate (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
+  Local Hint Extern 1 (opt.compile_item_data _ _) => simple apply (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
   Context (compiled_productions : list (opt.productions state))
           (Hcompiled_productions : List.map opt.compile_productions (List.map snd (pregrammar_productions G)) = compiled_productions).
 

diff --git a/src/Parsers/GenericRecognizerMin.v b/src/Parsers/GenericRecognizerMin.v
@@ -181,7 +181,7 @@ Section recursive_descent_parser.
                try unfold x'; try unfold y'
         end.
 
-      Local Hint Resolve (fun n m => proj1 (Nat.eqb_eq n m)) : generic_parser_correctness.
+      Local Hint Extern 1 (eq _ _) => simple apply (fun n m => proj1 (Nat.eqb_eq n m)) : generic_parser_correctness.
 
       Local Ltac eq_t' :=
         first [ progress subst_le_proof

diff --git a/src/Parsers/Refinement/PossibleTerminalsSets.v b/src/Parsers/Refinement/PossibleTerminalsSets.v
@@ -433,7 +433,7 @@ Local Declare Reduction opt_possible :=
 Section defs.
   Context (G : pregrammar' Ascii.ascii)
           {pdata : possible_data G}.
-  Local Hint Immediate (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
+  Local Hint Extern 1 (opt.compile_item_data _ _) => simple apply (compile_item_data_of_abstract_interpretation G) : typeclass_instances.
 
   Definition characters_set_to_ascii_list (s : PositiveSet.t)
     : list Ascii.ascii

diff --git a/src/Parsers/Reflective/LogicalRelations.v b/src/Parsers/Reflective/LogicalRelations.v
@@ -167,7 +167,9 @@ Hint Rewrite <- @interp_Term_syntactify_list @interp_Term_syntactify_nat @List.m
 #[global]
 Hint Rewrite @nth'_nth List.map_nth List.map_map List.map_length List.map_id @combine_map_r @combine_map_l @first_index_default_map Bool.orb_true_r Bool.orb_true_l Bool.andb_true_l Bool.andb_true_r Bool.orb_false_r Bool.orb_false_l Bool.andb_false_l Bool.andb_false_r BoolFacts.andbr_andb BoolFacts.orbr_orb @bool_rect_nodep_const @BoolFacts.uneta_bool_rect_nodep : partial_unfold_hints.
 #[global]
-Hint Resolve map_ext_in fold_left_app (@constantOf_correct cbool) @first_index_default_first_index_partial : partial_unfold_hints.
+Hint Resolve map_ext_in fold_left_app @first_index_default_first_index_partial : partial_unfold_hints.
+#[global]
+Hint Extern 1 (eq (interp_Term _) _) => eapply (@constantOf_correct cbool) : partial_unfold_hints.
 
 Local Ltac meaning_tac_helper' :=
   idtac;