aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/validator/Automaton.v
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/validator/Automaton.v')
-rw-r--r--cparser/validator/Automaton.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v
index b15f87d2..98ab1246 100644
--- a/cparser/validator/Automaton.v
+++ b/cparser/validator/Automaton.v
@@ -113,7 +113,7 @@ Module Types(Import Init:AutInit).
(** Types used for the annotations of the automaton. **)
(** An item is a part of the annotations given to the validator.
- It is acually a set of LR(1) items sharing the same core. It is needed
+ It is acually a set of LR(1) items sharing the same core. It is needed
to validate completeness. **)
Record item := {
(** The pseudo-production of the item. **)
@@ -136,7 +136,7 @@ Module Type T.
Parameter start_nt: initstate -> nonterminal.
(** The action table maps a state to either a map terminal -> action. **)
- Parameter action_table:
+ Parameter action_table:
state -> action.
(** The goto table of an LR(1) automaton. **)
Parameter goto_table: state -> forall nt:nonterminal,