From 025720092d7a095478a5f4572a90d0c106175797 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 9 Apr 2010 09:51:11 +0000 Subject: Granting wish #2249 (checking existing lemma name also when in a section). Simplified in passing generation of names for the "Goal" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/lemmas.ml | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'toplevel/lemmas.ml') diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 247fbbc0a..f80fbf201 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -185,19 +185,16 @@ let save_named opacity = let default_thm_id = id_of_string "Unnamed_thm" -let compute_proof_name = function +let compute_proof_name locality = function | Some (loc,id) -> (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || + locality=Global && Nametab.exists_cci (Lib.make_path_except_section id) + then user_err_loc (loc,"",pr_id id ++ str " already exists."); id | None -> - let rec next avoid id = - let id = next_global_ident_away id avoid in - if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id - else id - in - next (Pfedit.get_all_proof_names ()) default_thm_id + next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = match body with @@ -318,7 +315,7 @@ let start_proof_com kind thms hook = let t', imps' = interp_type_evars_impls ~evdref env t in Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx; let len = List.length ctx in - (compute_proof_name sopt, + (compute_proof_name (fst kind) sopt, (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'), guard))) -- cgit v1.2.3