diff options
| -rw-r--r-- | pretyping/termops.ml | 15 | ||||
| -rw-r--r-- | toplevel/command.ml | 10 |
2 files changed, 12 insertions, 13 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c0144cab4b..f0a781cf0b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -817,29 +817,22 @@ let names_of_rel_context env = (**** Globality of identifiers *) -(* TODO temporary hack!!! *) let rec is_imported_modpath = function - | MPfile dp -> dp <> (Lib.library_dp ()) -(* | MPdot (mp,_) -> is_imported_modpath mp *) - | _ -> false + | MPfile dp -> true + | p -> false let is_imported_ref = function | VarRef _ -> false | IndRef (kn,_) - | ConstructRef ((kn,_),_) -(* | ModTypeRef ln *) -> + | ConstructRef ((kn,_),_) -> let (mp,_,_) = repr_kn kn in is_imported_modpath mp -(* | ModRef mp -> - is_imported_modpath mp -*) | ConstRef kn -> let (mp,_,_) = repr_con kn in is_imported_modpath mp let is_global id = try let ref = locate (make_short_qualid id) in - not (is_imported_ref ref) || - (try ignore(locate (make_qualid (dirpath_of_string "Top") id)); true with _ -> false) + not (is_imported_ref ref) with Not_found -> false diff --git a/toplevel/command.ml b/toplevel/command.ml index 3b68780b74..413146ca7d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1052,6 +1052,8 @@ let retrieve_first_recthm = function (Option.map Declarations.force body,opaq) | _ -> assert false +let default_thm_id = id_of_string "Unnamed_thm" + let compute_proof_name = function | Some (loc,id) -> (* We check existence here: it's a bit late at Qed time *) @@ -1059,8 +1061,12 @@ let compute_proof_name = function user_err_loc (loc,"",pr_id id ++ str " already exists."); id | None -> - next_global_ident_away false (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) + let rec next avoid id = + let id = next_global_ident_away false 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 let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = match body with |