diff options
| author | Pierre-Marie Pédrot | 2016-04-11 11:02:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-11 11:02:27 +0200 |
| commit | 907db7ee1c9824aeedad7ce2d0f4f85225c36aba (patch) | |
| tree | 801a44dde07b604fcf5fa9d1e28270fe7319d4c6 /ltac | |
| parent | c6a8c4b5fa590f2beecd73817497bd7773a87522 (diff) | |
| parent | 2da7bf6327e1f35321f121de9560604b758f0472 (diff) | |
Removing the typed-level tactic_expr type.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6f0297268d..02b03b72c2 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1650,7 +1650,7 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic = | Some e -> Proofview.tclUNIT e | None -> Proofview.tclENV end >>= fun env -> - let name () = Pptactic.pr_tactic env (TacAtom (Loc.ghost,tacexpr)) in + let name () = Pptactic.pr_atomic_tactic env tacexpr in Proofview.Trace.name_tactic name tac (* Interprets a primitive tactic *) @@ -1769,7 +1769,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let tac = Option.map (interp_tactic ist) t in Tacticals.New.tclWITHHOLES false (name_atomic ~env - (TacAssert(b,t,ipat,c)) + (TacAssert(b,Option.map ignore t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma end } | TacGeneralize cl -> @@ -1951,7 +1951,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let cl = interp_clause ist env sigma cl in name_atomic ~env - (TacRewrite (ev,l,cl,by)) + (TacRewrite (ev,l,cl,Option.map ignore by)) (Equality.general_multi_rewrite ev l' cl (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) |