diff options
| author | Emilio Jesus Gallego Arias | 2020-04-21 13:45:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 18:05:14 +0200 |
| commit | ad84e6948a86db491a00bb92ec3e00a9a743b1f9 (patch) | |
| tree | 7a85b4dfe31bfc26b97baaa6acd306e9ff144bb8 | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
[declare] Remove fix_exn internal access.
| -rw-r--r-- | vernac/declare.ml | 13 | ||||
| -rw-r--r-- | vernac/declare.mli | 4 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 7 |
3 files changed, 11 insertions, 13 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 95e573a671..458002f03c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -495,6 +495,17 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = register_constant kn kind local in kn +let get_cd_fix_exn = function + | DefinitionEntry de -> + Future.fix_exn_of de.proof_entry_body + | _ -> fun x -> x + +let declare_constant ?local ~name ~kind cd = + try declare_constant ?local ~name ~kind cd + with exn -> + let exn = Exninfo.capture exn in + Exninfo.iraise (get_cd_fix_exn cd exn) + let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = @@ -620,8 +631,6 @@ module Internal = struct let set_opacity ~opaque entry = { entry with proof_entry_opaque = opaque } - let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body - let rec decompose len c t accu = let open Constr in let open Context.Rel.Declaration in diff --git a/vernac/declare.mli b/vernac/declare.mli index a297f25868..df81291e7e 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -211,10 +211,6 @@ module Internal : sig (* Overriding opacity is indeed really hacky *) val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - (* TODO: This is only used in DeclareDef to forward the fix to - hooks, should eventually go away *) - val get_fix_exn : 'a proof_entry -> Future.fix_exn - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list type constant_obj diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1809c2bc91..90d88b95a2 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -59,13 +59,6 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref -let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry - with exn -> - let exn = Exninfo.capture exn in - let fix_exn = Declare.Internal.get_fix_exn entry in - Exninfo.iraise (fix_exn exn) - let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> |