diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index fe4e9f6aa..71ee29f8c 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -25,7 +25,7 @@ open Redexpr (* Values for interpretation *) type value = - | VRTactic of (goal list sigma * validation) + | VRTactic of (goal list sigma) | VFun of ltac_trace * (identifier*value) list * identifier option list * glob_tactic_expr | VVoid |