From 990c96e18ca31781484f558d46c94537b5ec59cf Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 3 Oct 2021 18:42:50 +0200
Subject: Synchronize vendored MenhirLib with upstream (#416)

It remains compatible with earlier Menhir versions.
---
 MenhirLib/Alphabet.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'MenhirLib/Alphabet.v')

diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
index cd849761..8381c014 100644
--- a/MenhirLib/Alphabet.v
+++ b/MenhirLib/Alphabet.v
@@ -37,7 +37,7 @@ Qed.
 Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
   fun x y => compare x y = Lt.
 
-Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+Global Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
   StrictOrder (comparableLt C).
 Proof.
 apply Build_StrictOrder.
@@ -53,7 +53,7 @@ apply compare_trans.
 Qed.
 
 (** nat is comparable. **)
-Program Instance natComparable : Comparable nat :=
+Global Program Instance natComparable : Comparable nat :=
   { compare := Nat.compare }.
 Next Obligation.
 symmetry.
@@ -79,7 +79,7 @@ apply (gt_trans _ _ _ H H0).
 Qed.
 
 (** A pair of comparable is comparable. **)
-Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+Global Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
   Comparable (A*B) :=
   { compare := fun x y =>
       let (xa, xb) := x in let (ya, yb) := y in
@@ -134,10 +134,10 @@ destruct H.
 rewrite compare_refl; intuition.
 Qed.
 
-Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+Global Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
 
 (** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
-Instance PairComparableLeibnizEq
+Global Instance PairComparableLeibnizEq
   {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
   {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
     ComparableLeibnizEq (PairComparable CA CB).
@@ -174,7 +174,7 @@ Class Numbered (A:Type) := {
   inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
 }.
 
-Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+Global Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
   { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |};
     AlphabetFinite :=
       {| all_list := fst (Pos.iter
@@ -224,7 +224,7 @@ Import OrderedType.
 
 Module Type ComparableM.
   Parameter t : Type.
-  Declare Instance tComparable : Comparable t.
+  Global Declare Instance tComparable : Comparable t.
 End ComparableM.
 
 Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
-- 
cgit