diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 23:54:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:27 +0200 |
| commit | 58630ad9a0b94a804a39a3d99f982965292692c7 (patch) | |
| tree | 0adadc2828cfeeaf122bf6086990997c8b72f2c1 /pretyping | |
| parent | 9367f1626afb080d10d425262dca705046a32933 (diff) | |
[api] Misctypes removal: miscellaneous aliases.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pattern.ml | 3 | ||||
| -rw-r--r-- | pretyping/patternops.mli | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 4 |
6 files changed, 8 insertions, 6 deletions
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 |