diff options
| author | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
| commit | a7af2f6571d007b6f83a1ec9252b52f69907a965 (patch) | |
| tree | 014747da5aa139b93c3c6d3e015499bbfb525541 /tactics | |
| parent | 92a294ca53752b61b0270a719826ffc759a25e8d (diff) | |
export_private_constants doesn't use the [constr in_univ_ctx] argument
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index c7581fb0e0..e1d2ccc3eb 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -299,7 +299,7 @@ let define_constant ~name cd = if not de.proof_entry_opaque then (* This globally defines the side-effects in the environment. *) let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in + let export = Global.export_private_constants eff.Evd.seff_private in let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in @@ -377,8 +377,8 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in + let ((body, uctx), eff) = Future.force de.proof_entry_body in + let export = Global.export_private_constants eff.Evd.seff_private in let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.proof_entry_universes with |