diff options
| author | Pierre-Marie Pédrot | 2020-07-04 20:02:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-08 00:20:42 +0200 |
| commit | 834c64015b608b8152e160d37e6f07a3106ff26b (patch) | |
| tree | bc761838af2979d760322a270930e18fea8cffe1 /pretyping/evarconv.ml | |
| parent | aba870c6b58b18bc1bd4711c379863a87bbf6d33 (diff) | |
Remove Evarutil.new_evar_instance from the API.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6880383a31..400acc25b6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1411,11 +1411,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = refresh_universes ~status:Evd.univ_flexible (Some true) env_evar_unf evd evty else evd, evty in - let (evd, ev) = new_evar_instance sign evd evty ~filter instance in - let evk = fst (destEvar evd ev) in + let (evd, evk) = new_pure_evar sign evd evty ~filter in evsref := (evk,evty,inst,prefer_abstraction)::!evsref; fixed := Evar.Set.add evk !fixed; - evd, ev + evd, mkEvar (evk, instance) in let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in if debug_ho_unification () then |