X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FGeneral.v;fp=src%2FGeneral.v;h=2d8a35c44e27fd42c54b5ad8f7bd6e50c0f7857c;hb=4359342db4052c77b802ce256856df71387e7a62;hp=7aefcf020ee6114dc3b2af3d22e5a0cd281c6a08;hpb=2a887b5df62e3202c859c953d83918872bda31e4;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index 7aefcf0..2d8a35c 100644
--- 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".