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/Automaton.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/Automaton.v')
| -rw-r--r-- | MenhirLib/Automaton.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/MenhirLib/Automaton.v b/MenhirLib/Automaton.v index d5a19f35..1975be4f 100644 --- a/MenhirLib/Automaton.v +++ b/MenhirLib/Automaton.v @@ -23,10 +23,10 @@ Module Type AutInit. (** The set of non initial state is considered as an alphabet. **) Parameter noninitstate : Type. - Declare Instance NonInitStateAlph : Alphabet noninitstate. + Global Declare Instance NonInitStateAlph : Alphabet noninitstate. Parameter initstate : Type. - Declare Instance InitStateAlph : Alphabet initstate. + Global Declare Instance InitStateAlph : Alphabet initstate. (** When we are at this state, we know that this symbol is the top of the stack. **) @@ -41,7 +41,7 @@ Module Types(Import Init:AutInit). | Init: initstate -> state | Ninit: noninitstate -> state. - Program Instance StateAlph : Alphabet state := + Global Program Instance StateAlph : Alphabet state := { AlphabetComparable := {| compare := fun x y => match x, y return comparison with | Init _, Ninit _ => Lt |