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

2 files changed, 11 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 =
diff --git a/library/lib.mli b/library/lib.mli
index eca3164e3..25c0e1b24 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -91,6 +91,9 @@ val sections_depth : unit -> int
 (** Are we inside an opened module type *)
 val is_module_or_modtype : unit -> bool
 val is_modtype : unit -> bool
+(* [is_modtype_strict] checks not only if we are in a module type, but
+   if the latest module started is a module type.  *)
+val is_modtype_strict : unit -> bool
 val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident