Be more clever when forcing the body of a translated cofix

erasure/theories/ECoInductiveToInductive.v

@@ -144,13 +144,13 @@ Section trans.
       end
     end.
 
-  Fixpoint remove_head_lazy (t : term) : option term :=
+  Fixpoint force_cofix_body (t : term) : term :=
     match t with
-    | tLazy t => Some t
+    | tLazy t => t
     | tCase ind c brs =>
-      brs' <- map_option_out (List.map (fun '(n, br) => br' <- remove_head_lazy br ;; ret (n, br')) brs) ;;
-      ret (tCase ind c brs')
-    | _ => None
+      let brs' := List.map (fun '(n, br) => (n, force_cofix_body br)) brs in
+      tCase ind c brs'
+    | _ => tForce t
     end.
 
   Definition mkLambdas nas t :=
@@ -163,7 +163,7 @@ Section trans.
 
   Definition hoist_head_lazy_def (t : def term) :=
     '(nas, body') <- decompose_n_lambdas Σ t.(rarg) t.(dbody) ;;
-    body'' <- remove_head_lazy (whnf Σ body');;
+    let body'' := force_cofix_body (whnf Σ body') in
     ret {| dname := t.(dname);
            rarg := t.(rarg);
            dbody := mkLambdas nas (tLazy body'') |}.

test-suite/erasure_live_test.v

@@ -428,7 +428,7 @@ Import MCMonadNotation MCOption.
 Definition whnf : option EAst.term :=
   match decomp with
   | None => None
-  | Some deco => remove_head_lazy (whnf Σrepeat (snd deco))
+  | Some deco => Some (force_cofix_body (whnf Σrepeat (snd deco)))
   end.
 
 Eval lazy in whnf.
@@ -442,10 +442,7 @@ Module maybe_ones.
   MetaCoq Quote Recursively Definition maybe_onesq := maybe_ones.
   Eval lazy in (EPretty.print_program (testp_eprogram maybe_onesq)).
 
-
-
-EAst.program
-
+End maybe_ones.
 
 (* 0.2s purely in the bytecode VM *)
 (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *)