aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc
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 /plugins/cc
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 'plugins/cc')
-rw-r--r--plugins/cc/cctac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index fca7d9851..150319f6b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -444,7 +444,7 @@ let cc_tactic depth additionnal_terms =
let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
let pr_missing (c, missing) =
- let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
let holes = List.init missing (fun _ -> hole) in
Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
in