diff options
| author | herbelin | 2003-10-13 08:46:23 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-13 08:46:23 +0000 |
| commit | b6cbbb30f6272f93e8d0c3de4da4165ad079109d (patch) | |
| tree | e1f6e57b31efeda1e228813726154837b8a4d7bd | |
| parent | 8c0a5f183b1c9cff8baddd7f71d18e1cf768a191 (diff) | |
Protection contre les noms de lemmes existant deja
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4607 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a7cac8ac68..fb95bdc345 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -630,12 +630,12 @@ let start_proof_com sopt kind (bl,t) hook = let id = match sopt with | Some id -> (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) then + if is_global id then errorlabstrm "start_proof" (pr_id id ++ str " already exists"); id | None -> - next_ident_away (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) + next_global_ident_away false (id_of_string "Unnamed_thm") + (Pfedit.get_all_proof_names ()) in let env = Global.env () in let c = interp_type Evd.empty env (generalize_rawconstr t bl) in |