diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg index 8b29da0e2..3efd45e9e 100644 --- a/erasure-plugin/src/g_metacoq_erasure.mlg +++ b/erasure-plugin/src/g_metacoq_erasure.mlg @@ -105,7 +105,7 @@ To show this help message type:\n\ MetaCoq Erase -help.\n\n\ Valid options:\n\ -typed : Run the typed erasure pipeline including a dearging phase. By default we run the pipeline without this phase.\n\ --unsafe : Run also partially verified passes of the pipeline. This includes the cofix to fix translation.\n\ +-unsafe : Run also partially verified passes of the pipeline. This includes the cofix to lazy translation.\n\ -time : Time each compilation phase\n\ -bypass-qeds : Bypass the use of Qed and quote opaque proofs. Beware, this can result in large memory\n\ consumption due to reification of large proof terms.\n\ diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index 4b038a62a..b43908c2f 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -31,7 +31,7 @@ Import EWcbvEval. Local Obligation Tactic := program_simpl. Record unsafe_passes := - { fix_to_lazy : bool; + { cofix_to_lazy : bool; reorder_constructors : bool; inlining : bool; unboxing : bool; @@ -53,7 +53,7 @@ Definition default_dearging_config := Definition make_unsafe_passes b := - {| fix_to_lazy := b; + {| cofix_to_lazy := b; reorder_constructors := b; inlining := b; unboxing := b; @@ -67,7 +67,7 @@ Definition all_unsafe_passes := make_unsafe_passes true. representation by reordering constructors or unboxing. *) Definition default_unsafe_passes := - {| fix_to_lazy := true; + {| cofix_to_lazy := true; reorder_constructors := false; inlining := true; unboxing := false; @@ -127,7 +127,7 @@ Program Definition optional_unsafe_transforms econf := let passes := econf.(enable_unsafe) in let efl := EConstructorsAsBlocks.switch_cstr_as_blocks (EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in - ETransform.optional_self_transform passes.(fix_to_lazy) + ETransform.optional_self_transform passes.(cofix_to_lazy) ((* Rebuild the efficient lookup table *) rebuild_wf_env_transform (efl := efl) false false ▷ (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)