diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-21 10:45:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-30 18:36:55 +0200 |
| commit | 8b302bfba8f98458087685c8d5fbca2cf647255f (patch) | |
| tree | 7534097143d330c48573aaa9e79e53b0e2dfa66d /vernac/vernacexpr.ml | |
| parent | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (diff) | |
Move interning the [hint_pattern] outside the Typeclasses hooks.
Close #7562.
[api] move hint_info ast to tactics.
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 *) |