aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d80810af5..539a953a1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,7 +324,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =
let ks =
List.fold_left
(fun ks b ->
- let (k,_) = new_isevar isevars env (substl ks b) CCI in (k::ks))
+ (new_isevar isevars env (substl ks b) CCI)::ks)
[] bs
in
if (list_for_all2eq