diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-31 10:52:13 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-31 10:52:13 +0200 |
commit | 22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (patch) | |
tree | 7c8a970f1f6c4712223ad9ee366783e89576e5e0 /vernac/vernacexpr.ml | |
parent | 4598a26890a896ddcf6cd30758ae07882e245a16 (diff) | |
parent | 8b302bfba8f98458087685c8d5fbca2cf647255f (diff) |
Merge PR #7564: Move interning the [hint_pattern] outside the Typeclasses hooks.
Diffstat (limited to 'vernac/vernacexpr.ml')
-rw-r--r-- | vernac/vernacexpr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index cf0da4de2..40fab1f9c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -119,11 +119,11 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = hint_pattern : 'a option } [@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] -type hint_info_expr = Typeclasses.hint_info_expr -[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] +type hint_info_expr = Hints.hint_info_expr +[@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] type hints_expr = Hints.hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -362,12 +362,12 @@ type nonrec vernac_expr = local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) - Typeclasses.hint_info_expr + Hints.hint_info_expr | VernacContext of local_binder_expr list | VernacDeclareInstances of - (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) + (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *) | VernacDeclareClass of reference (* inductive or definition name *) |