diff options
| author | Matthieu Sozeau | 2014-10-15 16:55:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 16:55:28 +0200 |
| commit | f8023074b3a82e8c8adb4ee380c07a68bdea5961 (patch) | |
| tree | 062f605c087b7b59501d468de08b0f5c20285a4a | |
| parent | 433431c073522b4251dda71b36da5b26f374d58e (diff) | |
Make use of unfolded primitive projections when elaborating match on a
primitive record.
| -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) (**********************************************************************) |