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 /vernac/declareDef.ml | |
| parent | 91171386f55a2d423d831a1ce96f9d621a5be141 (diff) | |
[sideeff] Don't use polymorphic equality to check for empty side-effects
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1607771598..601e7e060c 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -171,7 +171,7 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let ce = definition_entry ?opaque ?inline ?types ~univs body in let env = Global.env () in let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); RetrieveObl.check_evars env sigma; let c = EConstr.of_constr c in |