diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:50:40 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:43 +0100 |
| commit | 20641795624dbb03da0401e4dc503660e5e73df6 (patch) | |
| tree | 3e4a94692a2c7ec1c722e8a8a3db94783a4cd684 /intf/vernacexpr.mli | |
| parent | 84f54fd0923c15109910123443348c193e37fe0f (diff) | |
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
Diffstat (limited to 'intf/vernacexpr.mli')
| -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 0e659459e..07a206b53 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: |