diff options
| -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 |