Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par

un nom importé) de la 8.2 vers le trunk.

--Cette ligne, et les suivantes ci-dessous, seront ignorées--

M    pretyping/termops.ml
M    toplevel/command.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11302 85f007b7-540e-0410-9357-904b9bb8a0f7

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