Merge pull request #36 from MetaRocq/allow-typed+unsafe

Allow running the unsafe passes after the typed extraction

Author: mattam82

theories/Pipeline.v

@@ -485,9 +485,16 @@ Arguments compile_malfunction_pipeline {_ _ _ _ _ _} _ _ _ {_}.
 Local Existing Instance CanonicalHeap.
 Local Existing Instance CanonicalPointer.
 
+Program Definition verified_typed_erasure_pipeline_unsafe econf :=
+  verified_typed_erasure_pipeline econf ▷ (optional_unsafe_transforms econf).
+Next Obligation.
+  unfold optional_unsafe_transforms, optional_self_transform in H |- *.
+  destruct enable_unsafe as [[] [] [] []] => //.
+Qed.
+
 (* This also optionally runs typed erasure and/or the cofix to fix translation *)
 Program Definition switchable_erasure_pipeline econf :=
-  if econf.(enable_typed_erasure) then verified_typed_erasure_pipeline econf
+  if econf.(enable_typed_erasure) then verified_typed_erasure_pipeline_unsafe econf
   else verified_erasure_pipeline_mapping ▷ (optional_unsafe_transforms econf).
 Next Obligation.
 Proof.