diff options
Diffstat (limited to 'toplevel/lemmas.ml')
| -rw-r--r-- | toplevel/lemmas.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7ea001259..d9a26b427 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -26,6 +26,7 @@ open Decl_kinds open Declare open Pretyping open Termops +open Namegen open Evd open Evarutil open Reductionops @@ -175,7 +176,7 @@ let compute_proof_name = function id | None -> let rec next avoid id = - let id = next_global_ident_away false id avoid in + let id = next_global_ident_away id avoid in if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id else id in |