Merge pull request #1065 from MetaCoq/fix-typo

Fix typo
MetaCoq · Mar 7, 2024 · 6037418 · 6037418
2 parents 9068e5b + ec34006
commit 6037418
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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 *)