Synchronize vendored MenhirLib with upstream (#416)

It remains compatible with earlier Menhir versions.

1 files changed, 6 insertions, 6 deletions

diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
index 781a6aa6..cced28ac 100644
--- a/MenhirLib/Validator_classes.v
+++ b/MenhirLib/Validator_classes.v
@@ -19,26 +19,26 @@ Class IsValidator (P : Prop) (b : bool) :=
   is_validator : b = true -> P.
 Global Hint Mode IsValidator + - : typeclass_instances.
 
-Instance is_validator_true : IsValidator True true.
+Global Instance is_validator_true : IsValidator True true.
 Proof. done. Qed.
 
-Instance is_validator_false : IsValidator False false.
+Global Instance is_validator_false : IsValidator False false.
 Proof. done. Qed.
 
-Instance is_validator_eq_true b :
+Global Instance is_validator_eq_true b :
   IsValidator (b = true) b.
 Proof. done. Qed.
 
-Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
+Global Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
   IsValidator (P1 /\ P2) (if b1 then b2 else false).
 Proof. by split; destruct b1, b2; apply is_validator. Qed.
 
-Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
+Global Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
   ComparableLeibnizEq C ->
   IsValidator (x = y) (compare_eqb x y).
 Proof. intros ??. by apply compare_eqb_iff. Qed.
 
-Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b :
+Global Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b :
   IsValidator P b ->
   IsValidator (x = y -> P) (if compare_eqb x y then b else true).
 Proof.