diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 19:53:51 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-10 18:11:02 -0400 |
| commit | 39c4f9030f3aefdb7581aa02dd4b0c0d1ef89ee5 (patch) | |
| tree | 9489b19632ba418a6dd9ef047543851eb069ebd4 /tactics | |
| parent | 91171386f55a2d423d831a1ce96f9d621a5be141 (diff) | |
[sideeff] Don't use polymorphic equality to check for empty side-effects
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/proof_global.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index d1c2467cce..98de0c848b 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -175,9 +175,11 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let opaque = match opaque with Opaque -> true | Transparent -> false in let make_entry ((body, eff), typ) = + let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + not poly && + (keep_body_ucst_separate + || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) in let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in |