diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 27340fe718..411f2c550f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1313,7 +1313,7 @@ let mk_case pb (ci,pred,c,brs) = match mib.mind_record with | Some (Some (_, cs, pbs)) -> Reduction.beta_appvect brs.(0) - (Array.map (fun p -> mkProj (Projection.make p false, c)) cs) + (Array.map (fun p -> mkProj (Projection.make p true, c)) cs) | _ -> mkCase (ci,pred,c,brs) (**********************************************************************) |