aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-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
5 files changed, 6 insertions, 7 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]