diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 15:45:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | 84eb5cd72a015c45337a5a6070c5651f56be6e74 (patch) | |
| tree | 6a54fa82bd711f37fa21f56dcce4591f9474b55c /plugins/ltac/tacinterp.ml | |
| parent | bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 (diff) | |
[location] Use located in tactics.
One case missing due the TACTIC EXTEND macro.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index aac63fcb2..64eda28ed 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1257,7 +1257,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) - | TacAlias (loc,s,l) -> + | TacAlias (loc,(s,l)) -> let (ids, body) = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in @@ -1341,9 +1341,9 @@ and interp_tacarg ist arg : Val.t Ftactic.t = let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } - | TacCall (loc,r,[]) -> + | TacCall (loc,(r,[])) -> interp_ltac_reference loc true ist r - | TacCall (loc,f,l) -> + | TacCall (loc,(f,l)) -> let (>>=) = Ftactic.bind in interp_ltac_reference loc true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> |