diff options
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f57b490fc4..7d7c4e3190 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1080,7 +1080,7 @@ let forward usetac ipat c gl = let t = refresh_universes (pf_type_of gl c) in tclTHENS (assert_as true ipat t) [exact_no_check c; tclIDTAC] gl | Some tac -> - tclTHENS (assert_as true ipat c) [tac; tclIDTAC] gl + tclTHENS (assert_as true ipat c) [tclCOMPLETE tac; tclIDTAC] gl (*****************************) (* High-level induction *) |