diff options
| author | herbelin | 2001-04-09 22:03:28 +0000 |
|---|---|---|
| committer | herbelin | 2001-04-09 22:03:28 +0000 |
| commit | b14e3ea6a7c2c50e2a1de3147ac5b364df383aac (patch) | |
| tree | e9617491873aab46ff34aff38f8ef85e1fdb3e31 | |
| parent | 1d3a24bec12a802be171135ddfb805dc4d0cdcee (diff) | |
Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1565 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index e8bc17cc34..baf99646c1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -463,7 +463,10 @@ let save_named opacity = let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then + error "This command can only be used for unnamed theorem" +(* message("Overriding name "^(string_of_id id)^" and using "^save_ident) +*) let save_anonymous opacity save_ident = let id,(const,strength) = Pfedit.cook_proof () in |