diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f98746a25..af4df3b6f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -149,12 +149,6 @@ GEXTEND Gram <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >> ] ] ; - gallina_ext: - [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]"; - ":="; c = constrarg -> - <:ast< (ABSTRACTION $id $c ($LIST $l)) >> - ] ] - ; END (* Gallina inductive declarations *) |