Assumption commands are now displayed as unsafe in Coqide.

They are still marked as safe if they are part of a module type, though.
Also local assumptions such as "Hypothesis" or "Context" are displayed
as unsafe if they happen to be defined without a section.

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

1 files changed, 8 insertions, 5 deletions

diff --git a/library/lib.ml b/library/lib.ml
index ac100b831..907d251e7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -365,18 +365,21 @@ let end_compilation dir =
 
 (* Returns true if we are inside an opened module or module type *)
 
-let is_module_gen which =
+let is_module_gen which check =
   let test = function
     | _, OpenedModule (ty,_,_,_) -> which ty
     | _ -> false
   in
   try
-    let _ = find_entry_p test in true
+    match find_entry_p test with
+    | _, OpenedModule (ty,_,_,_) -> check ty
+    | _ -> assert false
   with Not_found -> false
 
-let is_module_or_modtype () = is_module_gen (fun _ -> true)
-let is_modtype () = is_module_gen (fun b -> b)
-let is_module () = is_module_gen (fun b -> not b)
+let is_module_or_modtype () = is_module_gen (fun _ -> true) (fun _ -> true)
+let is_modtype () = is_module_gen (fun b -> b) (fun _ -> true)
+let is_modtype_strict () = is_module_gen (fun _ -> true) (fun b -> b)
+let is_module () = is_module_gen (fun b -> not b) (fun _ -> true)
 
 (* Returns the opening node of a given name *)
 let find_opening_node id =