diff options
| author | Maxime Dénès | 2018-11-29 15:37:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-13 10:08:02 +0100 |
| commit | e20a12d92c7cc7c40ee0ac0b6569b0ee5e0e0b0f (patch) | |
| tree | 1c9d80fb70c9df0a28e7fc8989e931cffb787b08 /plugins | |
| parent | d9a6d4814f0669b586ca5c13d6d6540cd194b45f (diff) | |
Move shallow state logic to the function preparing state for workers
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5d0d17ee6b..f9938c0356 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -492,7 +492,7 @@ type tcc_lemma_value = (* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> let e = CErrors.push e in |