aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/validator/Validator_safe.v
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/validator/Validator_safe.v')
-rw-r--r--cparser/validator/Validator_safe.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v
index 119f7337..c5229ac9 100644
--- a/cparser/validator/Validator_safe.v
+++ b/cparser/validator/Validator_safe.v
@@ -121,7 +121,7 @@ Qed.
Definition goto_head_symbs :=
forall s nt,
match goto_table s nt with
- | Some (exist s2 _) =>
+ | Some (exist s2 _) =>
prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
| None => True
end.