diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-08 02:11:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-10 18:22:27 +0100 |
| commit | e69aad0acf0ae1892ff62dc639389a7c88e66772 (patch) | |
| tree | 72ed8fd5cb95530220a52f741bffc1964f49d319 | |
| parent | 033ffae9beb88e8b9c509cf151331f5855165f2f (diff) | |
Useless Array.of_list
| -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) |