diff options
| author | Pierre-Marie Pédrot | 2019-10-13 16:15:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-13 16:15:37 +0200 |
| commit | 7f039cac07526881da1a149b8c0e49be32c2e89e (patch) | |
| tree | ff8cf5617e038e67f896006c27d5fa730dca7af8 /tactics | |
| parent | 564f265bfda10a2c6d4e7297dec47a14ad4b61b3 (diff) | |
| parent | b9ccd6f93ff1a0a0cf9f53030af66dd761a1315a (diff) | |
Merge PR #10862: Simplify universe handling wrt side effects: rm demote_seff_univs
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 5be7b4fa28..413c6540a3 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 -> @@ -141,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body in - let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = |