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 c1a23755cc..886620bc95 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -258,7 +258,7 @@ let next_global_ident_away id avoid = next_global_ident_from (lift_ident id) avoid let fresh_id avoid id gl = - next_ident_away id (avoid@(pf_ids_of_hyps gl)) + next_global_ident_away id (avoid@(pf_ids_of_hyps gl)) let id_of_name_with_default s = function | Anonymous -> id_of_string s |