improve HaskProofToStrong, although its messier now

[coq-hetmet.git] / src / General.v

diff --git a/src/General.v b/src/General.v
index 7aefcf0..2d8a35c 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -792,4 +792,16 @@ Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
 
 
 
+
+
+Record FreshMonad {T:Type} :=
+{ FMT       :  Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT       : FreshMonad >-> Funclass.
+
+
+
 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".