aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Remove declarations of matched variables in change as an extension ofGravatar Matthieu Sozeau2015-04-13
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Reverting r10021 which enforces early assumptions on freshness whichGravatar Hugo Herbelin2015-03-07
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* [info_auto] & [info_trivial]: warning message to help users find [Info].Gravatar Arnaud Spiwack2015-02-24
* [info] tactical warning: do not suggest [info_auto] and [info_trivial].Gravatar Arnaud Spiwack2015-02-24
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Remove compatibility layer from Ltac's [fail].Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing the previous commit. We had to normalize evars first.Gravatar Pierre-Marie Pédrot2014-11-20
* Somehow fixing a side-effect bug in tactics-in-terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr]-s in [idtac] messages.Gravatar Arnaud Spiwack2014-11-19
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3803.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing the unused boolean flag from the move tactic implementation.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Print [rename] tactic properly in info trace.Gravatar Arnaud Spiwack2014-11-07
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Info: the warning message of the defunct [info] tactic now points to the [Inf...Gravatar Arnaud Spiwack2014-11-01
* Info: print name of calls to Ltac constants ([TacCall]).Gravatar Arnaud Spiwack2014-11-01
* Info: tactic notations (TacAlias) print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: Tactics coming from [TACTIC EXTEND] print their names.Gravatar Arnaud Spiwack2014-11-01
* Info: print the name of atomic tactics.Gravatar Arnaud Spiwack2014-11-01
* Info: Ltac's idtac logs its message in the info trace.Gravatar Arnaud Spiwack2014-11-01
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 21:08:48 +0000