diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> | 2021-10-03 18:42:50 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-03 18:42:50 +0200 |
| commit | 990c96e18ca31781484f558d46c94537b5ec59cf (patch) | |
| tree | d4b610952733c6d2dfcf674cb289e74c1624f038 /MenhirLib/Alphabet.v | |
| parent | a2a2529d78b86ece65cfc03fa8670538b85bc991 (diff) | |
| download | compcert-kvx-990c96e18ca31781484f558d46c94537b5ec59cf.tar.gz compcert-kvx-990c96e18ca31781484f558d46c94537b5ec59cf.zip | |
Synchronize vendored MenhirLib with upstream (#416)
It remains compatible with earlier Menhir versions.
Diffstat (limited to 'MenhirLib/Alphabet.v')
| -rw-r--r-- | MenhirLib/Alphabet.v | 14 |
1 files changed, 7 insertions, 7 deletions
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. |