The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

Just use "Defined" instead of "Save".
"Save" or "Qed" is intended for theorems, which are not supposed
to be unfolded (they are opaque).

I would prefer that the Coq vernacular enforces the use of "Defined"
with "Definition" and "Qed" (or "Save", less clear imho) with
"Theorem" ("Lemma", etc.).

  Jean-Francois Monin

Michel Levy wrote:
> Could you explain me what is an evaluable constant, more exactly, why I
> can "Unfold h" directly defined by
> Definition h :=  [H:bool]H  : bool->bool
> 
> and why it's impossible when I defined f with a proof.
> I give a short sequence leading to this situation :
> 
> Coq < Definition f : bool -> bool.
> 1 subgoal
>   
>   ============================
>    bool->bool
> 
> f < Intro H; Assumption.
> Subtree proved!
> 
> f < Save.