diff options
| author | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
| commit | cc9856e33fa1a15fe699e8d9cd7b76086563683d (patch) | |
| tree | 3a51c6466ff40685d2c126a3997390c227b2ce8b /tactics | |
| parent | 5d82451d6d6f591ad81919d8e6529cee48474b9e (diff) | |
| parent | afd214869f050d07f9774d770c289bdc6e602dfd (diff) | |
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 3590146dfb..61321cd605 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -249,14 +249,13 @@ let is_unsafe_typing_flags () = let define_constant ~side_effect ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with | DefinitionEntry de -> (* We deal with side effects *) 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 ~in_section (body, eff.Evd.seff_private) in + let body, export = Global.export_private_constants (body, 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 @@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd = | PrimitiveEntry e -> [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false in - let kn, eff = Global.add_constant ~side_effect ~in_section name decl in + let kn, eff = Global.add_constant ~side_effect name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn, eff, export @@ -319,7 +318,7 @@ let declare_variable ~name ~kind d = (* 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 ~in_section:true (body, eff.Evd.seff_private) in + let ((body, uctx), export) = Global.export_private_constants (body, 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 @@ -585,7 +584,7 @@ let declare_univ_binders gr pl = Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) let do_universe ~poly l = - let in_section = Lib.sections_are_opened () in + let in_section = Global.sections_are_opened () in let () = if poly && not in_section then CErrors.user_err ~hdr:"Constraint" |