diff options
| author | Pierre-Marie Pédrot | 2016-04-10 02:37:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-11 10:59:23 +0200 |
| commit | 2da7bf6327e1f35321f121de9560604b758f0472 (patch) | |
| tree | 801a44dde07b604fcf5fa9d1e28270fe7319d4c6 /ltac | |
| parent | 4ebc7c27f04f2bcc3cf7160ae9ec177d1ca11707 (diff) | |
Removing the ad-hoc tactic_expr type.
This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.
Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.
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) |