diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 18:05:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 18:05:31 +0000 |
| commit | 45aeeae98cca32fb474fba4d36c529a50f90a16b (patch) | |
| tree | c2c4e37bf40c968db898c63ec4bd0dad42949729 /tactics | |
| parent | ee90aac584d123fa709d6629d99057b62bb343d0 (diff) | |
Granting wish 1794 (the name provided in the "using" clause of the
"abstract" tactical is now as a regular ltac parameter of the
"identifier" type).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a403832ff..24149a98e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1589,7 +1589,9 @@ and eval_tactic ist = function | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s) | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s) | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) - | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac) + | TacAbstract (tac,ido) -> + fun gl -> Tactics.tclABSTRACT + (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl | TacThen (t1,tf,t,tl) -> tclTHENS3PARTS (interp_tactic ist t1) (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) |