diff options
| author | Gaëtan Gilbert | 2019-10-09 15:00:55 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-09 15:02:21 +0200 |
| commit | ba86025e97d3ee110978592239131865f4187b1c (patch) | |
| tree | bd94d57b60d97564158364f5c507c54c3cb00bda /tactics | |
| parent | 0d744fce46a86c359aed902cd4c7ab647b8c9dc4 (diff) | |
Simplify universe handling wrt side effects: rm demote_seff_univs
We don't need to call `UState.demote_seff_univs` as
`emit_side_effects` (`tclEFFECTS`) can do it for us.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 5be7b4fa28..f7634ba745 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -124,8 +124,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac = let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in - entry, status, univs + entry, status, universes | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") with reraise -> |