diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d6b10b7d0..272225aca 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -482,15 +482,15 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = in ise_and evd' [(fun i -> - ise_list2 i - (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u)) - us2 us); - (fun i -> ise_list2 i (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x)) params1 params); - (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1); - (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))] + (fun i -> + ise_list2 i + (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u)) + us2 us); + (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks)))); + (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1)] (* We assume here |l1| <= |l2| *) |