From 46b59c60152148c122ee6ac26cddca42ae4f8430 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 29 Jan 2018 10:55:16 +0100
Subject: [native_compute] Fix evaluation of cofixpoints under primitive
 projections.

---
 kernel/nativecode.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ffe19510a6..613b2f2ec0 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1919,15 +1919,17 @@ let compile_constant env sigma prefix ~interactive con cb =
       let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
 		  asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
+      let cf_uid = fresh_lname Anonymous in
       let _, arity = tbl.(0) in
       let ci_uid = fresh_lname Anonymous in
       let cargs = Array.init arity
         (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None)
       in
       let i = push_symbol (SymbConst con) in
-      let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in
+      let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in
-      let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+      let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
       let gn = Gproj ("",con) in
       let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in
       let arg = fargs.(pb.proj_npars) in
-- 
cgit v1.2.3


From 60cb1f81e475d4b0f044a56ec4de503e42bad99a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 29 Jan 2018 11:11:35 +0100
Subject: [cbv] Fix evaluation of cofixpoints under primitive projections.

Fixes #5286 (last remaining part).
---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 4be607ec6c0b89e85566b4a6952bdf41e40fae7b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 29 Jan 2018 16:04:54 +0100
Subject: Add test case for #5286.

---
 test-suite/bugs/closed/5286.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/5286.v

diff --git a/test-suite/bugs/closed/5286.v b/test-suite/bugs/closed/5286.v
new file mode 100644
index 0000000000..98d4e5c968
--- /dev/null
+++ b/test-suite/bugs/closed/5286.v
@@ -0,0 +1,9 @@
+Set Primitive Projections.
+
+CoInductive R := mkR { p : unit }.
+
+CoFixpoint foo := mkR tt.
+
+Check (eq_refl tt : p foo = tt).
+Check (eq_refl tt <: p foo = tt).
+Check (eq_refl tt <<: p foo = tt).
-- 
cgit v1.2.3