diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evar_kinds.ml | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/uState.mli | 4 | ||||
| -rw-r--r-- | engine/univNames.ml | 2 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
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] |