diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 91 | ||||
| -rw-r--r-- | tactics/declare.mli | 8 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 2 |
3 files changed, 59 insertions, 42 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 9a14f4d40f..ce2f3ec2c5 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -130,8 +130,8 @@ let dummy_constant cst = { let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with +let (objConstant : constant_obj Libobject.Dyn.tag) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } +let inConstant v = Libobject.Dyn.Easy.inj v objConstant + let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -158,6 +160,18 @@ let register_side_effect (c, role) = | None -> () | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let export_side_effects eff = + let export = Global.export_private_constants eff.Evd.seff_private in + let export = get_roles export eff in + List.iter register_side_effect export + let record_aux env s_ty s_bo = let open Environ in let in_ty = keep_hyps env s_ty in @@ -276,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo opaque_entry_universes = univs; } -let get_roles export eff = - let map c = - let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in - (c, role) - in - List.map map export - let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = @@ -291,37 +298,36 @@ let is_unsafe_typing_flags () = let define_constant ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - 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 (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 - export, ConstantEntry cd, false - else - let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.proof_entry_body map in - let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry EffectEntry de in - [], OpaqueEntry de, false - | ParameterEntry e -> - [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) - | PrimitiveEntry e -> - [], ConstantEntry (Entries.PrimitiveEntry e), false + let decl, unsafe = match cd with + | DefinitionEntry de -> + (* We deal with side effects *) + if not de.proof_entry_opaque then + let body, eff = Future.force de.proof_entry_body in + (* This globally defines the side-effects in the environment + and registers their libobjects. *) + let () = export_side_effects eff in + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let cd = Entries.DefinitionEntry (cast_proof_entry de) in + ConstantEntry cd, false + else + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_opaque_proof_entry EffectEntry de in + OpaqueEntry de, false + | ParameterEntry e -> + ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) + | PrimitiveEntry e -> + ConstantEntry (Entries.PrimitiveEntry e), false in let kn = Global.add_constant name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); - kn, export + kn let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in - let kn, export = define_constant ~name cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in + let kn = define_constant ~name cd in + (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn @@ -357,10 +363,12 @@ type variable_declaration = (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) -let inVariable : unit -> obj = - declare_object { (default_object "VARIABLE") with +let objVariable : unit Libobject.Dyn.tag = + declare_object_full { (default_object "VARIABLE") with classify_function = (fun () -> Dispose)} +let inVariable v = Libobject.Dyn.Easy.inj v objVariable + let declare_variable ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then @@ -373,10 +381,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 eff = get_roles export eff in - let () = List.iter register_side_effect eff in + let ((body, uctx), eff) = Future.force de.proof_entry_body in + let () = export_side_effects eff in let poly, univs = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx @@ -497,4 +503,9 @@ module Internal = struct ; proof_entry_type = Some typ }, args + type nonrec constant_obj = constant_obj + + let objVariable = objVariable + let objConstant = objConstant + end diff --git a/tactics/declare.mli b/tactics/declare.mli index c646d2f85b..00c1e31717 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -131,7 +131,8 @@ val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) -(* For legacy support, do not use *) +(** {6 For legacy support, do not use} *) + module Internal : sig val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry @@ -145,4 +146,9 @@ module Internal : sig val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + type constant_obj + + val objConstant : constant_obj Libobject.Dyn.tag + val objVariable : unit Libobject.Dyn.tag + end diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 3c9803432a..a4a06873b8 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") + | NoSuchGoal -> Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end |