diff options
Diffstat (limited to 'ltac/tauto.ml')
| -rw-r--r-- | ltac/tauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index a86fdb98a..fa65a02b4 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -99,7 +99,7 @@ let intro = Tactics.intro let assert_ ?by c = let tac = match by with | None -> None - | Some tac -> Some (tclCOMPLETE tac) + | Some tac -> Some (Some tac) in Proofview.tclINDEPENDENT (Tactics.forward true tac None c) |