diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 0e659459e9..07a206b53e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -386,7 +386,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list + | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -453,6 +453,10 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr +and tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: |