diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 6e32d70c09..d566dd9b23 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -104,8 +104,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = | None -> mkCase (ci, lift ndepar p, mkRel 1, Termops.rel_vect ndepar k) | Some ps -> - let term = mkApp (mkRel 2, - Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in + let term = + mkApp (mkRel 2, + Array.map + (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in if dep then let ty = mkApp (mkRel 3, [| mkRel 1 |]) in mkCast (term, DEFAULTcast, ty) |