aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/library/states.ml b/library/states.ml
index 9d15dfc6c..eb597670f 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -23,8 +23,6 @@ let (extern_state,intern_state) =
extern_intern Coq_config.state_magic_number in
(fun s ->
let s = ensure_suffix s in
- if !Flags.load_proofs <> Flags.Force then
- Errors.error "Write State only works with option -force-load-proofs";
raw_extern s (freeze())),
(fun s ->
let s = ensure_suffix s in