diff options
| author | Hugo Herbelin | 2015-02-20 13:34:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-20 13:34:20 +0100 |
| commit | b092acdcf929af3b16f8445c8e5bb0ced52c3346 (patch) | |
| tree | a76b7e7f87c94397e6b04cfa1e9bfd884e576000 | |
| parent | bbafae3cc88452d89314342aa745705b4481d584 (diff) | |
Fixing error message when H already exists in tactic subexpression eqn:H.
| -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 |