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/Grammar.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'MenhirLib/Grammar.v') diff --git a/MenhirLib/Grammar.v b/MenhirLib/Grammar.v index 9be374e8..35ccbd8b 100644 --- a/MenhirLib/Grammar.v +++ b/MenhirLib/Grammar.v @@ -18,8 +18,8 @@ Require Import Alphabet. (** The terminal non-terminal alphabets of the grammar. **) Module Type Alphs. Parameters terminal nonterminal : Type. - Declare Instance TerminalAlph: Alphabet terminal. - Declare Instance NonTerminalAlph: Alphabet nonterminal. + Global Declare Instance TerminalAlph: Alphabet terminal. + Global Declare Instance NonTerminalAlph: Alphabet nonterminal. End Alphs. (** Definition of the alphabet of symbols, given the alphabet of terminals @@ -30,7 +30,7 @@ Module Symbol(Import A:Alphs). | T: terminal -> symbol | NT: nonterminal -> symbol. - Program Instance SymbolAlph : Alphabet symbol := + Global Program Instance SymbolAlph : Alphabet symbol := { AlphabetComparable := {| compare := fun x y => match x, y return comparison with | T _, NT _ => Gt @@ -74,7 +74,7 @@ Module Type T. (** The type of productions identifiers **) Parameter production : Type. - Declare Instance ProductionAlph : Alphabet production. + Global Declare Instance ProductionAlph : Alphabet production. (** Accessors for productions: left hand side, right hand side, and semantic action. The semantic actions are given in the form -- cgit