diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-29 11:11:35 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-29 16:02:59 +0100 |
| commit | 60cb1f81e475d4b0f044a56ec4de503e42bad99a (patch) | |
| tree | d4bd1f72304e71db8501dd91a6ee186356c4702b /pretyping/cbv.ml | |
| parent | 46b59c60152148c122ee6ac26cddca42ae4f8430 (diff) | |
[cbv] Fix evaluation of cofixpoints under primitive projections.
Fixes #5286 (last remaining part).
Diffstat (limited to 'pretyping/cbv.ml')
| -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 192eca63b..e42576d95 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 |