diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-12 15:42:49 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-12 15:42:49 +0000 |
| commit | 667e4a7870625bc8dedb651b278cbca4f43e793d (patch) | |
| tree | cef23852d980ae4e14d51ae38e7e76489864fff8 /parsing | |
| parent | b5676df44002aa6a347f58e455af780996ed407a (diff) | |
Ajout du vernac Proof with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 |
2 files changed, 7 insertions, 12 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 951e75815..879ce98ae 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -36,6 +36,7 @@ GEXTEND Gram (*VernacGoal c*) (* | IDENT "Goal" -> VernacGoal None*) | "Proof" -> VernacNop + | "Proof"; "with"; ta = tactic -> VernacProof ta (* Used ?? | IDENT "Begin" -> VernacNop *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 57d799a15..b4f7abbb0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -39,7 +39,9 @@ GEXTEND Gram | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c - | n = natural; ":"; v = goal_vernac; "." -> v n + | n = natural; ":"; tac = Tactic.tactic; "." -> VernacSolve (n,tac,true) + | n = natural; ":"; tac = Tactic.tactic; "!!" -> VernacSolve (n,tac,false) + | n = natural; ":"; v = check_command; "." -> v (Some n) | "["; l = vernac_list_tail -> VernacList l (* For translation from V7 to V8 *) @@ -52,10 +54,7 @@ GEXTEND Gram *) ] ] ; - goal_vernac: - [ [ tac = Tactic.tactic -> fun n -> VernacSolve (n,tac) - | v = check_command -> fun n -> v (Some n) ] ] - ; + check_command: [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr -> fun g -> VernacCheckMayEval (Some r, g, c) @@ -66,13 +65,8 @@ GEXTEND Gram [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] ; vernac: LAST - [ [ tac = Tactic.tactic; "." -> - (match tac with -(* Horrible hack pour LETTOP ! - | VernacSolve (Coqast.Node(_,kind,_)) - when kind = "StartProof" || kind = "TheoremProof" -> ?? -*) - | _ -> VernacSolve (1,tac)) + [ [ tac = Tactic.tactic; "." -> VernacSolve (1,tac,true) + | tac = Tactic.tactic; "!!" -> VernacSolve (1,tac,false) | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) ] ] |