Skip to content

Commit 576c5b6

Browse files
authored
Merge pull request #33 from ppedrot/namegen-no-global
Adapt w.r.t. rocq-prover/rocq#20423.
2 parents 3ee7d8b + 0dde07b commit 576c5b6

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/lean.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -791,7 +791,7 @@ let name_for n i =
791791
else
792792
(* prevent resetting the number *)
793793
let base = if i = 0 then base else Id.of_string (Id.to_string base ^ "_") in
794-
Namegen.next_global_ident_away base Id.Set.empty
794+
Namegen.next_global_ident_away (Global.safe_env ()) base Id.Set.empty
795795

796796
let get_predeclared_ind indn n i =
797797
if N.equal n (N.append_list N.anon indn) then
@@ -1408,7 +1408,7 @@ and declare_ind n { params; ty; ctors; univs } i =
14081408
match na.Context.binder_name with
14091409
| Names.Anonymous -> (ids, (na, t))
14101410
| Names.Name id ->
1411-
let id = Namegen.next_global_ident_away id ids in
1411+
let id = Namegen.next_global_ident_away (Global.safe_env ()) id ids in
14121412
let ids = Id.Set.add id ids in
14131413
line_msg
14141414
(N.of_list

0 commit comments

Comments
 (0)