aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-21 23:54:55 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-12 14:42:27 +0200
commit58630ad9a0b94a804a39a3d99f982965292692c7 (patch)
tree0adadc2828cfeeaf122bf6086990997c8b72f2c1
parent9367f1626afb080d10d425262dca705046a32933 (diff)
[api] Misctypes removal: miscellaneous aliases.
-rw-r--r--engine/evar_kinds.ml3
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/uState.mli4
-rw-r--r--engine/univNames.ml2
-rw-r--r--engine/univNames.mli2
-rw-r--r--interp/constrexpr.ml2
-rw-r--r--interp/constrintern.ml8
-rw-r--r--interp/constrintern.mli1
-rw-r--r--interp/declare.mli2
-rw-r--r--interp/dumpglob.mli4
-rw-r--r--interp/genredexpr.ml2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/implicit_quantifiers.mli4
-rw-r--r--interp/reserve.mli2
-rw-r--r--kernel/names.ml6
-rw-r--r--kernel/names.mli6
-rw-r--r--library/declaremods.ml1
-rw-r--r--library/declaremods.mli2
-rw-r--r--library/misctypes.ml12
-rw-r--r--plugins/ltac/g_tactic.ml49
-rw-r--r--plugins/ltac/pltac.mli6
-rw-r--r--plugins/ltac/tactic_debug.mli2
-rw-r--r--pretyping/pattern.ml3
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typeclasses_errors.ml2
-rw-r--r--pretyping/typeclasses_errors.mli4
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli6
-rw-r--r--vernac/comFixpoint.ml1
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/egramcoq.ml2
-rw-r--r--vernac/indschemes.mli6
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/metasyntax.mli1
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli4
39 files changed, 66 insertions, 68 deletions
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 6e123d642..12e2fda8e 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Misctypes
(** The kinds of existential variable *)
@@ -18,7 +17,7 @@ open Misctypes
type obligation_definition_status = Define of bool | Expand
-type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
type subevar_kind = Domain | Codomain | Body
diff --git a/engine/uState.ml b/engine/uState.ml
index 643c621fd..0e3ecdbf5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -312,7 +312,7 @@ type ('a, 'b) gen_universe_decl = {
univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+ (lident list, Univ.Constraint.t) gen_universe_decl
let default_univ_decl =
{ univdecl_instance = [];
diff --git a/engine/uState.mli b/engine/uState.mli
index e2f25642e..e7e5b39e0 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,7 +26,7 @@ val empty : t
val make : UGraph.t -> t
-val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
val is_empty : t -> bool
@@ -145,7 +145,7 @@ type ('a, 'b) gen_universe_decl = {
univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+ (lident list, Univ.Constraint.t) gen_universe_decl
val default_univ_decl : universe_decl
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6e59a7c9e..6ffb4bcf0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -89,7 +89,7 @@ let register_universe_binders ref ubinders =
if not (Id.Map.is_empty ubinders)
then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
let universe_binders_with_opt_names ref levels = function
| None -> universe_binders_of_global ref
diff --git a/engine/univNames.mli b/engine/univNames.mli
index e3bc3193d..c19aa19d5 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -29,7 +29,7 @@ val empty_binders : universe_binders
val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
val universe_binders_of_global : Names.GlobRef.t -> universe_binders
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
(** [universe_binders_with_opt_names ref u l]
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index ca6ea94f0..d6b395e01 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -95,7 +95,7 @@ and constr_expr_r =
| CIf of constr_expr * (lname option * constr_expr option)
* constr_expr * constr_expr
| CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
- | CPatVar of patvar
+ | CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr cast_type
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e09b7a793..057e10c00 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -606,7 +606,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id'
type binder_action =
-| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
+| AddLetIn of lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -1073,11 +1073,11 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
- | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
+ | RCPatAlias of 'a raw_cases_pattern_expr * lname
| RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
- | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+ | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1385,7 +1385,7 @@ let sort_fields ~complete loc fields completer =
(** {6 Manage multiple aliases} *)
type alias = {
- alias_ids : Misctypes.lident list;
+ alias_ids : lident list;
alias_map : Id.t Id.Map.t;
}
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4dd719e1f..12f77af30 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -11,7 +11,6 @@
open Names
open Evd
open Environ
-open Misctypes
open Libnames
open Glob_term
open Pattern
diff --git a/interp/declare.mli b/interp/declare.mli
index 4a9f54278..02e73cd66 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,6 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
-val do_universe : polymorphic -> Misctypes.lident list -> unit
+val do_universe : polymorphic -> lident list -> unit
val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
unit
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index bf83d2df4..931d05a97 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -27,7 +27,7 @@ val continue : unit -> unit
val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
-val dump_definition : Misctypes.lident -> bool -> string -> unit
+val dump_definition : Names.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
@@ -39,7 +39,7 @@ val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint : Misctypes.lname -> bool -> string -> unit
+val dump_constraint : Names.lname -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 80697461a..983493b25 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen =
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of Misctypes.lident * 'a
+ | ConstrContext of Names.lident * 'a
| ConstrTypeOf of 'a
open Libnames
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b48db9ac5..b54e2badd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -53,7 +53,7 @@ let cache_generalizable_type (_,(local,cmd)) =
let load_generalizable_type _ (_,(local,cmd)) =
generalizable_table := add_generalizable cmd !generalizable_table
-let in_generalizable : bool * Misctypes.lident list option -> obj =
+let in_generalizable : bool * lident list option -> obj =
declare_object {(default_object "GENERALIZED-IDENT") with
load_function = load_generalizable_type;
cache_function = cache_generalizable_type;
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index e64c5c542..25394fc0d 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,7 +13,7 @@ open Glob_term
open Constrexpr
open Libnames
-val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
@@ -31,7 +31,7 @@ val free_vars_of_binders :
order with the location of their first occurrence *)
val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
- glob_constr -> Misctypes.lident list
+ glob_constr -> lident list
val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index daee58639..a10858e71 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -11,5 +11,5 @@
open Names
open Notation_term
-val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
+val declare_reserved_type : lident list -> notation_constr -> unit
val find_reserved_type : Id.t -> notation_constr
diff --git a/kernel/names.ml b/kernel/names.ml
index 54f089e60..597061278 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -852,3 +852,9 @@ let eq_egr e1 e2 = match e1, e2 with
EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
| EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
| _, _ -> false
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/kernel/names.mli b/kernel/names.mli
index f988b559a..4eb5adb62 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -605,3 +605,9 @@ type evaluable_global_reference =
| EvalConstRef of Constant.t
val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/library/declaremods.ml b/library/declaremods.ml
index e8d89f96b..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} *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 63b25c7e4..b42a59bfb 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 a12caef80..3b629f449 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 =
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 15db4ca6a..038d55e4b 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -11,6 +11,7 @@
open Pp
open CErrors
open Util
+open Names
open Tacexpr
open Genredexpr
open Constrexpr
@@ -383,19 +384,19 @@ GEXTEND Gram
;
hypident:
[ [ id = id_or_meta ->
- let id : Misctypes.lident = id in
+ let id : lident = id in
id,InHyp
| "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
- let id : Misctypes.lident = id in
+ let id : lident = id in
id,InHypTypeOnly
| "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
- let id : Misctypes.lident = id in
+ let id : lident = id in
id,InHypValueOnly
] ]
;
hypident_occ:
[ [ (id,l)=hypident; occs=occs ->
- let id : Misctypes.lident = id in
+ let id : lident = id in
((occs,id),l) ] ]
;
in_clause:
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 434feba95..de23d2f8e 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -20,7 +20,7 @@ open Misctypes
val open_constr : constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
-val hypident : (lident * Locus.hyp_location_flag) Gram.entry
+val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
val uconstr : constr_expr Gram.entry
@@ -29,8 +29,8 @@ val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.ent
val int_or_var : int or_var Gram.entry
val simple_tactic : raw_tactic_expr Gram.entry
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : lident Locus.clause_expr Gram.entry
-val clause_dft_concl : lident Locus.clause_expr Gram.entry
+val in_clause : Names.lident Locus.clause_expr Gram.entry
+val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
val tactic_arg : raw_tactic_arg Gram.entry
val tactic_expr : raw_tactic_expr Gram.entry
val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 734e76b56..175341df0 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
(** Prints a logic failure message for a rule *)
val db_breakpoint : debug_info ->
- Misctypes.lident message_token list -> unit Proofview.NonLogical.t
+ lident message_token list -> unit Proofview.NonLogical.t
val extract_ltac_trace :
?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 996a2dc36..519a5466b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -13,6 +13,9 @@ open Misctypes
(** {5 Patterns} *)
+(** Cases pattern variables *)
+type patvar = Id.t
+
type case_info_pattern =
{ cip_style : Constr.case_style;
cip_ind : inductive option;
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index dfbfb147f..36317b3ac 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -10,7 +10,6 @@
open Names
open Mod_subst
-open Misctypes
open Glob_term
open Pattern
open EConstr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 70588b6ad..d3aa7ac64 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
let typeclasses_unique_solutions = ref false
let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c78382c82..e4a56960c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
(** This module defines type-classes *)
type typeclass = {
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a1ac53c73..2720a3e4d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -18,7 +18,7 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
- | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
+ | UnboundMethod of GlobRef.t * lident (* Class name, method *)
exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 1003f2ae1..9831627a9 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -16,11 +16,11 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
- | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
+ | UnboundMethod of GlobRef.t * lident (** Class name, method *)
exception TypeClassError of env * typeclass_error
val not_a_class : env -> constr -> 'a
-val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
+val unbound_method : env -> GlobRef.t -> lident -> 'a
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 05f48ec79..89df8f5b9 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -39,7 +39,7 @@ val pr_name : Name.t -> Pp.t
[@@ocaml.deprecated "alias of Names.Name.print"]
val pr_qualid : qualid -> Pp.t
-val pr_patvar : patvar -> Pp.t
+val pr_patvar : Pattern.patvar -> Pp.t
val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 946379356..3120c97b5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,7 +83,7 @@ type opacity_flag = Opaque | Transparent
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
| Proved of opacity_flag *
- Misctypes.lident option *
+ lident option *
proof_object
type proof_terminator = proof_ending -> unit
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0141cacb9..9e07ed2d0 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
val get_current_proof_name : unit -> Names.Id.t
val get_all_proof_names : unit -> Names.Id.t list
-val discard : Misctypes.lident -> unit
+val discard : Names.lident -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
@@ -54,7 +54,7 @@ type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
UState.t
| Proved of opacity_flag *
- Misctypes.lident option *
+ Names.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
@@ -126,7 +126,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
* (w.r.t. type dependencies and let-ins covered by it) + a list of
* ids to be cleared *)
val set_used_variables :
- Names.Id.t list -> Context.Named.t * Misctypes.lident list
+ Names.Id.t list -> Context.Named.t * Names.lident list
val get_used_variables : unit -> Context.Named.t option
(** Get the universe declaration associated to the current proof. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b5b8697d2..1d1cc62de 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -13,7 +13,6 @@ open Decl_kinds
open Pretyping
open Evarutil
open Evarconv
-open Misctypes
module RelDecl = Context.Rel.Declaration
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a6992a30b..f51bfbad5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -33,7 +33,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : Constrexpr.universe_decl_expr option;
- fix_annot : Misctypes.lident option;
+ fix_annot : lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e7a308dda..434e836d8 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -228,7 +228,7 @@ type _ target =
type prod_info = production_level * production_position
type (_, _) entry =
-| TTName : ('self, Misctypes.lname) entry
+| TTName : ('self, lname) entry
| TTReference : ('self, reference) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index bd4249cac..261c3d813 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -32,17 +32,17 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Misctypes.lident * bool * inductive * Sorts.family) list -> unit
+ (lident * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
-val do_scheme : (Misctypes.lident option * scheme) list -> unit
+val do_scheme : (lident option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
-val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit
+val do_combined_scheme : lident -> lident list -> unit
(** Hook called at each inductive type definition *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2245e762f..8f64f5519 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -92,7 +92,7 @@ let pr_grammar = function
(* Parse a format (every terminal starting with a letter or a single
quote (except a single quote alone) must be quoted) *)
-let parse_format ({CAst.loc;v=str} : Misctypes.lstring) =
+let parse_format ({CAst.loc;v=str} : lstring) =
let len = String.length str in
(* TODO: update the line of the location when the string contains newlines *)
let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in
@@ -792,7 +792,7 @@ type notation_modifier = {
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : Misctypes.lstring option;
+ format : lstring option;
extra : (string * string) list;
}
@@ -1104,7 +1104,7 @@ module SynData = struct
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : Misctypes.lstring option;
+ format : lstring option;
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index a6c12e089..f6de75b07 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -14,7 +14,6 @@ open Notation
open Constrexpr
open Notation_term
open Environ
-open Misctypes
val add_token_obj : string -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 00f1760c2..1ab24b670 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -298,10 +298,10 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
-type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type program_info_aux = {
prg_name: Id.t;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1eaf51ac..a37c30aaf 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -62,10 +62,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
- (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+ (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
val add_mutual_definitions :