1 files changed, 0 insertions, 85 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v
deleted file mode 100644
index dd9785b5..00000000
--- a/mppa_k1c/abstractbb/Impure/ImpConfig.v
+++ /dev/null
@@ -1,85 +0,0 @@
-(** Impure Config for UNTRUSTED backend !!! *)
-
-Require Import ImpMonads.
-Require Extraction.
-(** Pure computations (used for extraction !) 
-
-We keep module [Impure] opaque in order to check that Coq proof do not depend on 
-the implementation of [Impure].
-
-*)
-
-Module Type ImpureView.
-
- Include MayReturnMonad.
-
-(* WARNING: THIS IS REALLY UNSAFE TO DECOMMENT THE "UnsafeImpure" module !
-
-   unsafe_coerce coerces an impure computation into a pure one !
-
-*)
-
-(* START COMMENT *)
- Module UnsafeImpure.
-
- Parameter unsafe_coerce: forall {A}, t A -> option A.
-
- Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x.
-
- Extraction Inline unsafe_coerce.
-
- End UnsafeImpure.
-(* END COMMENT *)
-
-
-End ImpureView.
-
-
-Module Impure: ImpureView.
-
-  Include IdentityMonad.
-
-  Module UnsafeImpure.
-
-  Definition unsafe_coerce {A} (x:t A) := Some x.
-
-  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x.
-  Proof.
-    unfold unsafe_coerce, mayRet; congruence.
-  Qed.
-
-  End UnsafeImpure.
-
-End Impure.
-
-
-(** Comment the above code and decomment this to test that coq proofs still work with an impure monad !
-
-- this should fail only on extraction or if unsafe_coerce is used !
-
-*)
-(*
-Module Impure: MayReturnMonad := PowerSetMonad.
-*)
-
-Export Impure.
-
-Extraction Inline ret mk_annot.
-
-
-(* WARNING. The following directive is unsound.
-
-  Extraction Inline bind
-
-For example, it may lead to extract the following code as "true" (instead of an error raising code)
-  failwith "foo";;true
-
-*)
-
-Extract Inlined Constant bind => "(|>)".
-
-
-Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *)
-Extraction Inline t.
-
-Global Opaque t.