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 1a80e9811..49af044c5 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -28,7 +28,7 @@ type value = | VFun of (identifier * value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int - | VIdentifier of identifier + | VIntroPattern of intro_pattern_expr | VConstr of constr | VConstr_context of constr | VRec of value ref |