diff options
| author | clrenard | 2001-11-19 15:44:31 +0000 |
|---|---|---|
| committer | clrenard | 2001-11-19 15:44:31 +0000 |
| commit | 00adc2896f49f36f6b88990335022d9fcd70e482 (patch) | |
| tree | 02572616b075aa4391280305e7307d8d2aa11705 /parsing | |
| parent | 79ac780518b797b9e2181ef3993cb08c202b130a (diff) | |
Diverses petites simplications de la machine de preuves.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 9d6455608b..57058961e6 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 -> |