From a3e890a390e9541045b1ce4c024fffcca275ff90 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 24 Aug 2012 10:14:49 +0000 Subject: 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 --- library/lib.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'library/lib.ml') 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 = -- cgit v1.2.3