diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-10 01:27:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-10 01:27:44 +0200 |
| commit | c6a8c4b5fa590f2beecd73817497bd7773a87522 (patch) | |
| tree | 4bcf5db0fdb721755b3aa3a04cb738011d276675 /intf | |
| parent | f8f2c684ce97745350f8cbcb654a2ee27fb9d572 (diff) | |
Expliciting the fact that the atomic tactic type is self-contained.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 0aa3b936c..f821251c2 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -191,7 +191,7 @@ constraint 'a = < (** Possible arguments of a tactic definition *) -and 'a gen_tactic_arg = +type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref |