diff options
| author | Pierre Roux | 2019-02-17 10:10:22 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-03-31 23:17:55 +0200 |
| commit | eadb00648127c9a535b533d51189dce41ef16db7 (patch) | |
| tree | 1e5db53e73950ca4c7d7d9ae5e01a5d5c83ac32f /plugins | |
| parent | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (diff) | |
Multiple payload types in tokens
Instead of just string (and empty strings for tokens without payload)
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index b770b97384..814be64f81 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -48,7 +48,7 @@ let atactic n = else Aentryl (Pltac.tactic_expr, string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name (** Quite ad-hoc *) let get_tacentry n m = |