diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-01 03:01:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-01 03:01:14 +0000 |
| commit | 50da43eaa170cd051de690d7a396d56060c60e87 (patch) | |
| tree | 6aeb41bc6bf8caed93704174a916afa48202ad6d | |
| parent | e48ac2fd2466f971f694a66be29c3a13d3184635 (diff) | |
Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage des variables
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1776 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 c1a23755c..886620bc9 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 |