diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index c660f403f..c40570c2c 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -535,8 +535,8 @@ module V82 = struct in let evi = Typeclasses.mark_unresolvable evi in let (evars, evk) = Evarutil.new_pure_evar_full evars evi in - let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in - let inst = Array.of_list (List.map mkVar ids) in + let ctxt = Environ.named_context_of_val hyps in + let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in let ev = Term.mkEvar (evk,inst) in (build evk, ev, evars) |