diff options
| author | Pierre-Marie Pédrot | 2015-10-18 20:29:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-18 23:26:41 +0200 |
| commit | 7d697193ab175b6bfa3c773880c0a06348449d19 (patch) | |
| tree | ea863b9f523e367add2dc832985a78ed14788fd7 /pretyping/evarconv.ml | |
| parent | 4a76d2034983462175219426ec47c45a3c60d4fe (diff) | |
Making Evarutil.new_evar monotonous.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d5bb564f66..60d92f4beb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -22,6 +22,7 @@ open Evarsolve open Globnames open Evd open Pretype_errors +open Sigma.Notations type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -830,7 +831,9 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (i,t2::ks, m-1, test) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in - let (i',ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in + let i = Sigma.Unsafe.of_evar_map i in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in + let i' = Sigma.to_evar_map i' in (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in |