From ebd7475829d5e6927622776507315249c622b6ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 10 Apr 2024 16:27:15 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#18895. (#110) --- src/Common/MSetExtensions.v | 2 +- .../ContextFreeGrammar/Fix/FromAbstractInterpretation.v | 2 +- .../Fix/FromAbstractInterpretationDefinitions.v | 2 +- src/Parsers/GenericRecognizerMin.v | 2 +- src/Parsers/Refinement/PossibleTerminalsSets.v | 2 +- src/Parsers/Reflective/LogicalRelations.v | 4 +++- 6 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Common/MSetExtensions.v b/src/Common/MSetExtensions.v index a61984153..959985f53 100644 --- 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 index 6b62d0687..57e57615f 100644 --- 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 index d8f0a738b..11f63726d 100644 --- 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 index e113d90f0..ee4ac2d07 100644 --- 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 index 8ffec0405..1f5a7dc27 100644 --- 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 index bdd1605b3..58d309c2f 100644 --- 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;