aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2018-12-21 11:39:55 +0100
committerMaxime Dénès2018-12-21 11:39:55 +0100
commit69f11d7d3f95e1281542ec0b792cc5afd3eccf78 (patch)
tree11394dffc105f60ce7028fc3051d1e59f114f751
parentba6b5839add7587837b4cea890f2d505ce76d489 (diff)
Fix shallow flag in vernac state
Was incorrect due to a leftover in #9220.
-rw-r--r--vernac/vernacstate.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index b40bccf27e..61540024ef 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -36,7 +36,8 @@ let do_if_not_cached rf f v =
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
- shallow = marshallable }
+ shallow = false;
+ }
let unfreeze_interp_state { system; proof } =
do_if_not_cached s_cache States.unfreeze system;