diff options
| author | Brian Campbell | 2019-01-24 14:48:31 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-01-24 14:57:35 +0000 |
| commit | 04f95f5bac9401c84fd401bd130d9e19b34c2a5c (patch) | |
| tree | 9fbb233e80a7cca28d2dde4396b4341e9626d47d /src | |
| parent | 69fec085c3c35f4834c28b92f418afa7960ca969 (diff) | |
Make recheck_defs_without_effects restore old flag properly
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 39f753ef..19ec6db7 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4966,9 +4966,10 @@ let rewrite_explicit_measure (Defs defs) = let recheck_defs defs = fst (Type_error.check initial_env defs) let recheck_defs_without_effects defs = + let old = !opt_no_effects in let () = opt_no_effects := true in let result,_ = Type_error.check initial_env defs in - let () = opt_no_effects := false in + let () = opt_no_effects := old in result let remove_mapping_valspecs (Defs defs) = |