diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 2b7b783666e348c39be550493b667afa7f92d230..6524c6ee03264845bdf3ceeab6e05f1ddf76ded1 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -1029,9 +1029,6 @@ for_clause: | declaration { FC_DECL $1 } ; -/* 01/12/2017: ghost_parameter_opt and ghost_parameter are parsed - then thrown -*/ ghost_parameter_opt: /* empty */ {[]} | ghost_parameter {$1}