aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-09 21:47:17 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-28 16:51:21 +0200
commitd28304f6ba18ad9527a63cd01b39a5ad27526845 (patch)
treeddd8c5d10f0d1e52c675e8e027053fac7f05f259 /vernac/record.ml
parentb9740771e8113cb9e607793887be7a12587d0326 (diff)
Efficient fresh name generation relying on sets.
The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
Diffstat (limited to 'vernac/record.ml')
-rw-r--r--vernac/record.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml
index 4fb607dec..18e7796ca 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -457,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let impls = implicits_of_context params in
List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
- let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
+ let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in
let impl, projs =
match fields with
| [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->