diff options
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3efb6393b5..e6b43a81e8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -285,7 +285,8 @@ let rec intro_gen name_flag move_flag force_flag gl = | IBasedOn (id,idl) -> fresh_id idl id gl | IMustBe id -> let id' = fresh_id [] id gl in - if id' <> id then error ((string_of_id id)^" is already used") + if id' <> id then error ((string_of_id id)^" is already used"); + id' in begin match move_flag with | None -> introduction id gl |