diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 7 | ||||
| -rw-r--r-- | library/declaremods.mli | 10 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | library/misctypes.ml | 114 |
4 files changed, 11 insertions, 121 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 1d5df49cf..0b3b461e6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,7 +17,6 @@ open Entries open Libnames open Libobject open Mod_subst -open Misctypes (** {6 Inlining levels} *) @@ -36,6 +35,8 @@ type inline = | DefaultInline | InlineAt of int +type module_kind = Module | ModType | ModAny + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function @@ -994,8 +995,8 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) type 'modast module_interpretor = - Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t type 'modast module_params = (lident list * ('modast * inline)) list diff --git a/library/declaremods.mli b/library/declaremods.mli index 4aee7feae..b42a59bfb 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -27,12 +27,16 @@ type inline = | DefaultInline | InlineAt of int +(** Kinds of modules *) + +type module_kind = Module | ModType | ModAny + type 'modast module_interpretor = - Environ.env -> Misctypes.module_kind -> 'modast -> - Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t + Environ.env -> module_kind -> 'modast -> + Entries.module_struct_entry * module_kind * Univ.ContextSet.t type 'modast module_params = - (Misctypes.lident list * ('modast * inline)) list + (lident list * ('modast * inline)) list (** [declare_module interp_modast id fargs typ exprs] declares module [id], with structure constructed by [interp_modast] diff --git a/library/library.mllib b/library/library.mllib index 1c0368847..2ac4266fc 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -6,7 +6,6 @@ Nametab Global Decl_kinds Lib -Misctypes Declaremods Loadpath Library diff --git a/library/misctypes.ml b/library/misctypes.ml deleted file mode 100644 index cfae07484..000000000 --- a/library/misctypes.ml +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) - -(** Located identifiers and objects with syntax. *) - -type lident = Id.t CAst.t -type lname = Name.t CAst.t -type lstring = string CAst.t - -(** Cases pattern variables *) - -type patvar = Id.t - -(** Introduction patterns *) - -type 'constr intro_pattern_expr = - | IntroForthcoming of bool - | IntroNaming of intro_pattern_naming_expr - | IntroAction of 'constr intro_pattern_action_expr -and intro_pattern_naming_expr = - | IntroIdentifier of Id.t - | IntroFresh of Id.t - | IntroAnonymous -and 'constr intro_pattern_action_expr = - | IntroWildcard - | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of ('constr intro_pattern_expr) CAst.t list - | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t - | IntroRewrite of bool -and 'constr or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list - | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list - -(** Move destination for hypothesis *) - -type 'id move_location = - | MoveAfter of 'id - | MoveBefore of 'id - | MoveFirst - | MoveLast (** can be seen as "no move" when doing intro *) - -(** A synonym of [Evar.t], also defined in Term *) - -type existential_key = Evar.t - -(** Casts *) - -type 'a cast_type = - | CastConv of 'a - | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) - | CastNative of 'a - -(** Bindings *) - -type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t - -type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list - -type 'a bindings = - | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_bindings - | NoBindings - -type 'a with_bindings = 'a * 'a bindings - - -(** Some utility types for parsing *) - -type 'a or_var = - | ArgArg of 'a - | ArgVar of lident - -type 'a and_short_name = 'a * lident option - -type 'a or_by_notation_r = - | AN of 'a - | ByNotation of (string * string option) - -type 'a or_by_notation = 'a or_by_notation_r CAst.t - -(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], - but this formulation avoids a useless dependency. *) - - -(** Kinds of modules *) - -type module_kind = Module | ModType | ModAny - -(** Various flags *) - -type direction_flag = bool (* true = Left-to-right false = right-to-right *) -type evars_flag = bool (* true = pose evars false = fail on evars *) -type rec_flag = bool (* true = recursive false = not recursive *) -type advanced_flag = bool (* true = advanced false = basic *) -type letin_flag = bool (* true = use local def false = use Leibniz *) -type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) - -type multi = - | Precisely of int - | UpTo of int - | RepeatStar - | RepeatPlus |