aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Expand)Author
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Reimplementing the clearbody tactic.Pierre-Marie Pédrot
2014-09-04Using goal-tactics to interpret arguments to idtac.Pierre-Marie Pédrot
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
2014-09-04Revert "Tacinterp: [interp_message] and associate now only require an environ...Pierre-Marie Pédrot
2014-09-04Revert "Ltac's idtac is now implemented using the new API."Pierre-Marie Pédrot
2014-09-04Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Pierre-Marie Pédrot
2014-09-02Removing [revert] tactic from the AST.Pierre-Marie Pédrot
2014-09-01Moving the decompose tactic out of the AST.Pierre-Marie Pédrot
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-27Removing spurious tclWITHHOLES.Pierre-Marie Pédrot
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-16Better printing of Ltac values.Pierre-Marie Pédrot
2014-08-15Removing unused Refiner.tclWITHHOLES.Pierre-Marie Pédrot
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-07Removing simple induction / destruct from the AST.Pierre-Marie Pédrot
2014-08-07Instead of relying on a trick to make the constructor tactic parse, putPierre-Marie Pédrot
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-08-06Revert the change in Constrintern introduced by "Add a type of untyped term t...Arnaud Spiwack
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-06Removing "intros untils" from the AST.Pierre-Marie Pédrot
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05Ltac's [idtac] is now interpreted outside of a goal if possible.Arnaud Spiwack
2014-08-05Ltac's idtac is now implemented using the new API.Arnaud Spiwack
2014-08-05Tacinterp: [interp_message] and associate now only require an environment rat...Arnaud Spiwack
2014-08-05Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Arnaud Spiwack
2014-08-05Fix interpretation bug in [uconstr].Arnaud Spiwack
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-08-02Better struture for Ltac internalization environments in Constrintern.Pierre-Marie Pédrot
2014-08-01New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Arnaud Spiwack
2014-08-01Add [numgoal] to Ltac.Arnaud Spiwack
2014-07-29Untyped terms in tactic: function [type_term c] to give a typed version of [c].Arnaud Spiwack
2014-07-29Add a type of untyped term to Ltac's value.Arnaud Spiwack
2014-07-29Clean up obsolete comment.Arnaud Spiwack
2014-07-28CPS-style tactic matching. We use the tactic monad as the target of the CPS.Pierre-Marie Pédrot
2014-07-25A slightly more fine grained way to check whether a TACTIC EXTEND is global o...Arnaud Spiwack
2014-07-24Distinguish tactics t1;t2 and t1;[t2..].Arnaud Spiwack
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-10Fix a oversight in 5bf9e67b .Arnaud Spiwack
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-07-03More efficient implementation of Ltac match, by inlining a stream map.Pierre-Marie Pédrot
2014-07-01Fixing the place where to insert a space in "Tactic failure"Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 08:20:52 +0000