diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 16:55:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:11 +0200 |
| commit | 6291e5b13e74ef3cd0b2354266352470f88cc70e (patch) | |
| tree | 9f7f8fbc5ed4fef62132054b4bd4203971762072 | |
| parent | c09871df35c75630f51f0495d715d46b7ad2733d (diff) | |
[declare] [compat] Remove exception alias.
| -rw-r--r-- | vernac/declare.ml | 3 | ||||
| -rw-r--r-- | vernac/declare.mli | 25 |
2 files changed, 11 insertions, 17 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index e72f5a0397..fc52c05793 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1184,9 +1184,6 @@ let prepare_parameter ~poly ~udecl ~types sigma = let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, (None(*proof using*), (typ, univs), None(*inline*)) -(* Compat: will remove *) -exception AlreadyDeclared = DeclareUniv.AlreadyDeclared - module Obls = struct open Constr diff --git a/vernac/declare.mli b/vernac/declare.mli index 4f6b2f70da..e0af3a7344 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -406,17 +406,6 @@ val fixpoint_message : int array option -> Id.t list -> unit val check_exists : Id.t -> unit -(** {6 For internal support, do not use} *) - -module Internal : sig - - type constant_obj - - val objConstant : constant_obj Libobject.Dyn.tag - val objVariable : unit Libobject.Dyn.tag - -end - (** Semantics of this function is a bit dubious, use with care *) val build_by_tactic : ?side_eff:bool @@ -437,9 +426,6 @@ val prepare_obligation -> Evd.evar_map -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info -(* Compat: will remove *) -exception AlreadyDeclared of (string option * Names.Id.t) - module Obls : sig type 'a obligation_body = DefinedObl of 'a | TermObl of constr @@ -545,3 +531,14 @@ val obl_substitution : val dependencies : Obligation.t array -> int -> Int.Set.t end + +(** {6 For internal support, do not use} *) + +module Internal : sig + + type constant_obj + + val objConstant : constant_obj Libobject.Dyn.tag + val objVariable : unit Libobject.Dyn.tag + +end |