diff options
| author | Maxime Dénès | 2018-01-30 10:01:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-30 10:01:50 +0100 |
| commit | 879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (patch) | |
| tree | b2775e675b9b82acd5fd8a34b99b7b33af782d91 /pretyping | |
| parent | ae2429e6cf0e4faa0e57bd3b1393efc3b532920a (diff) | |
| parent | 4be607ec6c0b89e85566b4a6952bdf41e40fae7b (diff) | |
Merge PR #6666: Fix reduction of primitive projections on coinductive records for cbv and native_compute
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 192eca63bb..e42576d95b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false |