diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-09 21:47:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-28 16:51:21 +0200 |
| commit | d28304f6ba18ad9527a63cd01b39a5ad27526845 (patch) | |
| tree | ddd8c5d10f0d1e52c675e8e027053fac7f05f259 /pretyping/detyping.mli | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (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 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 67c852af3..b70bfd83c 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -35,16 +35,16 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr +val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g +val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g val detype_sort : evar_map -> sorts -> glob_sort -val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list -val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr +val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option |