Commit c8facadd authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix compatibility with Coq 8.10/master, and fix Coq 8.10 warnings.

parent dfce23df
Pipeline #85855 passed with stages
in 25 seconds
......@@ -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
......
......@@ -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. split; destruct b1, b2; by 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, _) _) =>
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment