diff options
Diffstat (limited to 'vernac/locality.ml')
-rw-r--r-- | vernac/locality.ml | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/vernac/locality.ml b/vernac/locality.ml index 054a451a4..681b1ab20 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -6,22 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp - (** * Managing locality *) let local_of_bool = function | true -> Decl_kinds.Local | false -> Decl_kinds.Global -let check_locality locality_flag = - match locality_flag with - | Some b -> - let s = if b then "Local" else "Global" in - CErrors.user_err ~hdr:"Locality.check_locality" - (str "This command does not support the \"" ++ str s ++ str "\" prefix.") - | None -> () - (** Extracting the locality flag *) (* Commands which supported an inlined Local flag *) @@ -95,13 +85,3 @@ let make_module_locality = function let enforce_module_locality locality_flag local = make_module_locality (enforce_locality_full locality_flag local) - -module LocalityFixme = struct - let locality = ref None - let set l = locality := l - let consume () = - let l = !locality in - locality := None; - l - let assert_consumed () = check_locality !locality -end |