diff options
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 6 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 2 |
4 files changed, 10 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 181ec4860c..50922ffc52 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -301,6 +301,7 @@ sig type t val repr : t -> side_effect list val empty : t + val is_empty : t -> bool val add : side_effect -> t -> t val concat : t -> t -> t end = @@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t } let repr eff = eff.seff let empty = { seff = []; elts = SeffSet.empty } +let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts let add x es = if SeffSet.mem x es.elts then es else { seff = x :: es.seff; elts = SeffSet.add x es.elts } @@ -349,6 +351,7 @@ let push_private_constants env eff = List.fold_left add_if_undefined env eff let empty_private_constants = SideEffects.empty +let is_empty_private_constants c = SideEffects.is_empty c let concat_private = SideEffects.concat let universes_of_private eff = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f8d5d319a9..b42746a882 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants val empty_private_constants : private_constants +val is_empty_private_constants : private_constants -> bool + val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) 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 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 |