diff options
| author | Pierre-Marie Pédrot | 2020-07-23 11:05:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | ed4159b617f49d3a024ac6e344c127d99208a0f7 (patch) | |
| tree | 339da243754fd0a4c67f1aa3d47090d16e776352 /engine | |
| parent | 7126990e5b04d51927f414b277124c127fb14887 (diff) | |
Actually update uninitialized evar instances (hum hum).
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 6bbfddd988..1c091d2c24 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -152,7 +152,10 @@ struct let make s = ref (Some s) let none () = ref None let repr sign filter s = match !s with - | None -> Filter.filter_list filter sign.env_named_var + | None -> + let ans = Filter.filter_list filter sign.env_named_var in + let () = s := Some ans in + ans | Some s -> s let is_identity l s = match !s with | None -> false |