From 415c5a5a28ac7035cfa33e5753af841a450bfab0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 6 Jul 2019 16:16:20 +0200
Subject: Fix compatibility with Coq 8.10 (#303)

The generation of some fresh names changes in Coq 8.10 (https://github.com/coq/coq/pull/9160).

The `Hint Mode` declaration that does not specify a hint database now triggers a warning.
Specify the intended database and fix the "auto" tactics accordingly.
---
 MenhirLib/Automaton.v         | 6 +++---
 MenhirLib/Validator_classes.v | 9 +++++----
 MenhirLib/Validator_safe.v    | 4 ++--
 3 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'MenhirLib')

diff --git a/MenhirLib/Automaton.v b/MenhirLib/Automaton.v
index c310fc61..d5a19f35 100644
--- a/MenhirLib/Automaton.v
+++ b/MenhirLib/Automaton.v
@@ -99,9 +99,9 @@ Module Types(Import Init:AutInit).
                  T term = last_symb_of_non_init_state s -> lookahead_action term
   | Reduce_act: production -> lookahead_action term
   | Fail_act: lookahead_action term.
-  Arguments Shift_act [term].
-  Arguments Reduce_act [term].
-  Arguments Fail_act [term].
+  Arguments Shift_act {term}.
+  Arguments Reduce_act {term}.
+  Arguments Fail_act {term}.
 
   Inductive action :=
   | Default_reduce_act: production -> action
diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
index c043cb73..d8063123 100644
--- a/MenhirLib/Validator_classes.v
+++ b/MenhirLib/Validator_classes.v
@@ -17,7 +17,7 @@ Require Import Alphabet.
 
 Class IsValidator (P : Prop) (b : bool) :=
   is_validator : b = true -> P.
-Hint Mode IsValidator + -.
+Hint Mode IsValidator + - : typeclass_instances.
 
 Instance is_validator_true : IsValidator True true.
 Proof. done. Qed.
@@ -31,7 +31,7 @@ Proof. done. Qed.
 
 Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
   IsValidator (P1 /\ P2) (if b1 then b2 else false).
-Proof. split; destruct b1, b2; auto using is_validator. Qed.
+Proof. by split; destruct b1, b2; apply is_validator. Qed.
 
 Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
   ComparableLeibnizEq C ->
@@ -49,9 +49,10 @@ Lemma is_validator_forall_finite A P b `(Finite A) :
   (forall (x : A), IsValidator (P x) (b x)) ->
   IsValidator (forall (x : A), P x) (forallb b all_list).
 Proof.
-  move=> ? /forallb_forall.
-  auto using all_list_forall, is_validator, forallb_forall.
+  move=> ? /forallb_forall Hb ?.
+  apply is_validator, Hb, all_list_forall.
 Qed.
+
 (* We do not use an instance directly here, because we need somehow to
    force Coq to instantiate b with a lambda. *)
 Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v
index 2d2ea4b3..628d2009 100644
--- a/MenhirLib/Validator_safe.v
+++ b/MenhirLib/Validator_safe.v
@@ -184,8 +184,8 @@ Instance impl_is_state_valid_after_pop_is_validator state sl pl P b :
   IsValidator (state_valid_after_pop state sl pl -> P)
               (if is_state_valid_after_pop state sl pl then b else true).
 Proof.
-  destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ.
-  - intros ??. auto using is_validator.
+  destruct (is_state_valid_after_pop _ sl pl) eqn:EQ.
+  - intros ???. by eapply is_validator.
   - intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|].
     by destruct sl.
 Qed.
-- 
cgit