The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Consider the following code in Mtac.

  Definition when_has_value1 (p: option Prop) :=
    match p with
      | None => True
      | Some p' => p'
    end.

  Definition when_has_value2 (p: M Prop) :=
    match p with
      | ret p' => p'
      |  _ => True (* there was an exception *)
    end.

The first function extracts a value from the option Monad -- if there is a prop, we return the prop. Otherwise, we return true.

The second definition attempts (but does not compile) to extract a value from the M monad -- however it doesn't work. I feel like I'm doing something ridiciously stupid and there's a trivial fix -- how do I get the second function to work?

Thanks!