diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 9d6455608..57058961e 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -77,14 +77,6 @@ GEXTEND Gram | IDENT "Show"; IDENT "Node" -> <:ast< (ShowNode) >> | IDENT "Show"; IDENT "Script" -> <:ast< (ShowScript) >> | IDENT "Show"; IDENT "Existentials" -> <:ast< (ShowEx) >> - | IDENT "Existential"; n = numarg; ":="; c = constrarg -> - <:ast< (EXISTENTIAL $n $c) >> - | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":"; - c2 = Constr.constr -> - <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> - | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":="; - c1 = Constr.constr -> - <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> | IDENT "Explain"; "Proof"; l = numarg_list -> <:ast< (ExplainProof ($LIST $l)) >> | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list -> |