aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/goal.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b1f8fd3e97..53d3047bc7 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -69,7 +69,7 @@ module V82 = struct
let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
let evars = Evd.restore_future_goals evars prev_future_goals in
let ctxt = Environ.named_context_of_val hyps in
- let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+ let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
let ev = EConstr.mkEvar (evk,inst) in
(evk, ev, evars)