From 990c96e18ca31781484f558d46c94537b5ec59cf Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 3 Oct 2021 18:42:50 +0200 Subject: Synchronize vendored MenhirLib with upstream (#416) It remains compatible with earlier Menhir versions. --- MenhirLib/Automaton.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'MenhirLib/Automaton.v') 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 -- cgit