diff options
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 74f5c4a649..013270b0bd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2318,7 +2318,10 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let heq = match ido with | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env - | IntroIdentifier id -> id in + | IntroIdentifier id -> + if List.mem id (ids_of_named_context (named_context env)) then + user_err_loc (loc,"",pr_id id ++ str" is already used."); + id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in let sigma, eq = Evd.fresh_global env sigma eqdata.eq in |