diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9dd71b75d2..0e26d170e4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1698,8 +1698,8 @@ let tclABSTRACT name_op tac gls = let dyn_tclABSTRACT = hide_tactic "ABSTRACT" (function - | [Tac tac] -> + | [Tac (tac,_)] -> tclABSTRACT None tac - | [Identifier s; Tac tac] -> + | [Identifier s; Tac (tac,_)] -> tclABSTRACT (Some s) tac | _ -> invalid_arg "tclABSTRACT") |