diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 18:46:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 12:58:15 +0200 |
| commit | 81545ec98255e644be589d34a521924549e9e2fa (patch) | |
| tree | 65ab59d21e680a00e379deffa440f038b5d0c121 /pretyping/typeclasses.ml | |
| parent | 0f107c8a747af6bdb40d70d80236f84b325dc35d (diff) | |
[api] Move `hint_info_expr` to `Typeclasses`.
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 30ddeffa6..e73a78fb8 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) +(* Core typeclasses hints *) +type 'a hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } + +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + let typeclasses_unique_solutions = ref false let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions @@ -73,7 +80,7 @@ type typeclass = { cl_props : Context.Rel.t; (* The method implementaions as projections. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option + cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list; cl_strict : bool; @@ -85,7 +92,7 @@ type typeclasses = typeclass Refmap.t type instance = { is_class: global_reference; - is_info: Vernacexpr.hint_info_expr; + is_info: hint_info_expr; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; @@ -96,7 +103,7 @@ type instances = (instance Refmap.t) Refmap.t let instance_impl is = is.is_impl -let hint_priority is = is.is_info.Vernacexpr.hint_priority +let hint_priority is = is.is_info.hint_priority let new_instance cl info glob impl = let global = @@ -266,8 +273,6 @@ let check_instance env sigma c = not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false -open Vernacexpr - let build_subclasses ~check env sigma glob { hint_priority = pri } = let _id = Nametab.basename_of_global glob in let _next_id = |