diff options
| author | Pierre-Marie Pédrot | 2016-04-25 16:22:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 16:26:35 +0200 |
| commit | cca1a283d4693ef75f2aa48fc07c4d51bcd108c7 (patch) | |
| tree | de075b506538c43a66f199f1403ea0a67536d0c1 /intf | |
| parent | 65578a55b81252e2c4b006728522839a9e37cd5c (diff) | |
| parent | 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 (diff) | |
Simplifying and uniformizing the implementation of tactic notations.
This branch mainly provides two features:
1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq
registration anymore. We expose instead an API to interpret names as a given
generic argument, effectively reversing the logical dependency between parsing
entries and generic arguments.
2. ML tactics do not declare their own notation system anymore. They rely instead
on plain tactic notations, except for a little hack due to the way we currently
interpret toplevel values.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index 10713745e4..381d47dd18 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -53,14 +53,14 @@ type simple_constr_prod_entry_key = (** {5 AST for user-provided entries} *) -type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +type 'a user_symbol = +| Ulist1 of 'a user_symbol +| Ulist1sep of 'a user_symbol * string +| Ulist0 of 'a user_symbol +| Ulist0sep of 'a user_symbol * string +| Uopt of 'a user_symbol +| Uentry of 'a +| Uentryl of 'a * int (** {5 Type-safe grammar extension} *) |