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/evardefine.ml | |
| 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/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 7f5a780f9..9fed28bb3 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -72,7 +72,7 @@ let define_pure_evar_as_product evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in + let id = next_ident_away idx (Context.Named.to_vars (evar_context evi)) in let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in let s = destSort evd concl in let evd1,(dom,u1) = @@ -127,7 +127,7 @@ let define_pure_evar_as_lambda env evd evk = | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in - let avoid = ids_of_named_context (evar_context evi) in + let avoid = Context.Named.to_vars (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in |