diff options
| author | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
| commit | eed90d1bd867dce59f6bf1b2bf769fff188f128b (patch) | |
| tree | cfbf3bb666b23d0ddce9ea3c370c54eb4a87a150 /plugins/ltac/tacsubst.ml | |
| parent | 23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff) | |
| parent | bbde815f8108f4641f5411d03f7a88096cc2221b (diff) | |
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4390ff08b4..f5e6f05cee 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -146,13 +146,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacAssert (b,otac,na,c) -> - TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na, + | TacAssert (ev,b,otac,na,c) -> + TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na, subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) + | TacLetTac (ev,id,c,clp,b,eqpat) -> + TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> |