diff options
| author | filliatr | 2000-10-27 16:28:55 +0000 |
|---|---|---|
| committer | filliatr | 2000-10-27 16:28:55 +0000 |
| commit | d4f8643a9f5aff3c0f819b4b7aafda4b782ef55d (patch) | |
| tree | fde5af24e5ed2c5069c5417e93b6b4ad1e5a17be | |
| parent | aaf2ca06f7f0ae5e7be30aaf5c5dcd6677bfb016 (diff) | |
erreur dans intro_gen corrigée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@777 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |