aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-07-04 20:02:42 +0200
committerPierre-Marie Pédrot2020-07-08 00:20:42 +0200
commit834c64015b608b8152e160d37e6f07a3106ff26b (patch)
treebc761838af2979d760322a270930e18fea8cffe1 /proofs
parentaba870c6b58b18bc1bd4711c379863a87bbf6d33 (diff)
Remove Evarutil.new_evar_instance from the API.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4d148756b4..9bd7ccda5d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -781,7 +781,8 @@ let make_evar_clause env sigma ?len t =
Some (ctx, args, subst), ctx, args, subst
| Some (ctx, args, subst) -> inst, ctx, args, subst
in
- let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in
+ let (sigma, ev) = new_pure_evar ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) in
+ let ev = mkEvar (ev, args) in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;