diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-01 19:45:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 13:12:13 +0100 |
| commit | 968dfdb15cc11d48783017b2a91147b25c854ad6 (patch) | |
| tree | d619d1ebe51d29e5517c9c0385dc4aefe546edbe /pretyping/evarconv.ml | |
| parent | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (diff) | |
Monotonizing the Evarutil module.
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 99e51330e..f3ff26876 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1007,7 +1007,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd,ev = new_evar_instance sign !evdref evty ~filter instance in + let evd = Sigma.Unsafe.of_evar_map !evdref in + let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in + let evd = Sigma.to_evar_map evd in evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in |