diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-10 02:21:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-28 16:51:21 +0200 |
| commit | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (patch) | |
| tree | 16dc8bc2ae1b5374a1329b9f6495d0a1b9905ee4 /pretyping/evardefine.ml | |
| parent | d28304f6ba18ad9527a63cd01b39a5ad27526845 (diff) | |
Efficient computation of the names contained in an environment.
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 9fed28bb3..5f12f360b 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 (Context.Named.to_vars (evar_context evi)) in + let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) 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 = Context.Named.to_vars (evar_context evi) in + let avoid = Environ.ids_of_named_context_val evi.evar_hyps 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 |