diff options
| author | herbelin | 2003-10-07 20:52:57 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-07 20:52:57 +0000 |
| commit | 2425dd9e258fe67e01bc63b0c2e82db0ecc3cdd6 (patch) | |
| tree | c4e478582aaefb3ebec25aa9c80008ca30ad3ccf /parsing | |
| parent | 9be9fa2e571532d32611e510f06b9197b004d459 (diff) | |
Debranchement de l'affichage automatique de Proof par le traducteur (trop complique de trouver la bonne indentation); affichage en revanche de Proof s'il existait deja
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4536 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f3ef4dc76c..11d70529d7 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -38,7 +38,7 @@ GEXTEND Gram [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c (*VernacGoal c*) (* | IDENT "Goal" -> VernacGoal None*) - | "Proof" -> VernacNop + | "Proof" -> VernacProof Tacexpr.TacId | "Proof"; "with"; ta = tactic -> VernacProof ta (* Used ?? | IDENT "Begin" -> VernacNop |