diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-23 11:59:44 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-23 11:59:44 +0000 |
| commit | 5f322bafad483d6868c385235f39d157e999051b (patch) | |
| tree | c2ef69fef5a4090469cb1cf3375bbf77ca4ec5fa /parsing | |
| parent | 2afbdd7b229eef8f4ee15363bedf84cd087d4257 (diff) | |
Retablissement de la commande Existential que j'avais supprime par erreur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2243 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 57058961e..fdd29feee 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -77,6 +77,14 @@ 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 -> |