aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Expand)Author
2016-03-20Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Improve error message.Maxime Dénès
2015-10-29Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Guillaume Melquiond
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-19Categorizing debug messages as such + NonLogical uses loggers.Pierre Courtieu
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-06-23Fixing incompatibility introduced with simpl in commit 364decf59c1 (orHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-04-13Remove declarations of matched variables in change as an extension ofMatthieu Sozeau
2015-04-10Fix #3590 for good this time, by changing the API, change's argument nowMatthieu Sozeau
2015-03-07Reverting r10021 which enforces early assumptions on freshness whichHugo Herbelin
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-24[info_auto] & [info_trivial]: warning message to help users find [Info].Arnaud Spiwack
2015-02-24[info] tactical warning: do not suggest [info_auto] and [info_trivial].Arnaud Spiwack
2015-02-10More expressive API for tclWITHHOLES.Pierre-Marie Pédrot
2015-02-10Revert "Removing spurious tclWITHHOLES."Pierre-Marie Pédrot
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Remove compatibility layer from Ltac's [fail].Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-20Fixing the previous commit. We had to normalize evars first.Pierre-Marie Pédrot
2014-11-20Somehow fixing a side-effect bug in tactics-in-terms.Pierre-Marie Pédrot
2014-11-19Print [uconstr]-s in [idtac] messages.Arnaud Spiwack
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-10Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Pierre-Marie Pédrot
2014-11-09Fixing bug #3803.Pierre-Marie Pédrot
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-07Print [rename] tactic properly in info trace.Arnaud Spiwack
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-11-01Info: the warning message of the defunct [info] tactic now points to the [Inf...Arnaud Spiwack
2014-11-01Info: print name of calls to Ltac constants ([TacCall]).Arnaud Spiwack
2014-11-01Info: tactic notations (TacAlias) print their names.Arnaud Spiwack
2014-11-01Info: Tactics coming from [TACTIC EXTEND] print their names.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:25:20 +0000