diff options
Diffstat (limited to 'plugins/ltac/taccoerce.ml')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 91d26519b8..f7037176d2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -394,7 +394,7 @@ type appl = (* Values for interpretation *) type tacvalue = - | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t * Name.t list * Tacexpr.glob_tactic_expr | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr |