From 2af78d3cca0f941841394b224b96f86903a68b10 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 20:40:27 +0200 Subject: [api] Misctypes removal: multi to tactics/rewrite --- library/misctypes.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'library') diff --git a/library/misctypes.ml b/library/misctypes.ml index cfae074843..ac8c7890cd 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -106,9 +106,3 @@ 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 -- cgit v1.2.3 From 9367f1626afb080d10d425262dca705046a32933 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 20:48:30 +0200 Subject: [api] Misctypes removal: module_kind to Declaremods --- library/declaremods.ml | 6 ++++-- library/declaremods.mli | 8 ++++++-- library/misctypes.ml | 6 ------ 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index 1d5df49cfd..e8d89f96b7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -36,6 +36,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 +996,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 4aee7feae9..63b25c7e40 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -27,9 +27,13 @@ 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 diff --git a/library/misctypes.ml b/library/misctypes.ml index ac8c7890cd..a12caef800 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -75,7 +75,6 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings - (** Some utility types for parsing *) type 'a or_var = @@ -93,11 +92,6 @@ 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 *) -- cgit v1.2.3 From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:54:55 +0200 Subject: [api] Misctypes removal: miscellaneous aliases. --- library/declaremods.ml | 1 - library/declaremods.mli | 2 +- library/misctypes.ml | 12 ------------ 3 files changed, 1 insertion(+), 14 deletions(-) (limited to 'library') diff --git a/library/declaremods.ml b/library/declaremods.ml index e8d89f96b7..0b3b461e6c 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} *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 63b25c7e40..b42a59bfbd 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -36,7 +36,7 @@ type 'modast module_interpretor = 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/misctypes.ml b/library/misctypes.ml index a12caef800..3b629f449f 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -10,18 +10,6 @@ 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 = -- cgit v1.2.3 From 36a98d55576ebdb106a55c3bd682961da8d77dee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:57:32 +0200 Subject: [api] Misctypes removal: remove dummy alias. --- library/misctypes.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'library') diff --git a/library/misctypes.ml b/library/misctypes.ml index 3b629f449f..7cd1a83be1 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -38,10 +38,6 @@ type 'id move_location = | 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 = -- cgit v1.2.3 From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- library/misctypes.ml | 86 ---------------------------------------------------- 1 file changed, 86 deletions(-) delete mode 100644 library/misctypes.ml (limited to 'library') diff --git a/library/misctypes.ml b/library/misctypes.ml deleted file mode 100644 index 7cd1a83be1..0000000000 --- a/library/misctypes.ml +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(*