diff options
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 29985d867..def78d92a 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -93,9 +93,8 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; (* bl = LIST0 binder; *) ":"; + [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":"; c = lconstr -> - let bl = [] in VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) |