aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
...
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr]-s in [idtac] messages.Gravatar Arnaud Spiwack2014-11-19
* Tentative rephrasing of error message for rewrite.Gravatar Hugo Herbelin2014-11-18
* Hopefully the last word on having "simpl f" complying with theGravatar Hugo Herbelin2014-11-18
* 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
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
* Renouncing to check only at the end of the call to "apply in" theGravatar Hugo Herbelin2014-11-11
* Replugging hints in rewriting strategies.Gravatar Pierre-Marie Pédrot2014-11-10
* 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
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
* Granting #3717 (more informative error message on missing arguments for funct...Gravatar Hugo Herbelin2014-11-07
* Fixing #3562 ("as" in "destruct" expects either a disjunctiveGravatar Hugo Herbelin2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Print [rename] tactic properly in info trace.Gravatar Arnaud Spiwack2014-11-07
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
* Dependency bug in using eqn for destruct.Gravatar Hugo Herbelin2014-11-06
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Subtle swap of lines to preserve VarInstance src field before checkingGravatar Hugo Herbelin2014-11-03
* Fix to 844431761 on improving elimination with indices, getting rid ofGravatar Hugo Herbelin2014-11-03
* Saving some nf_evars in the code of destruct/induction.Gravatar Hugo Herbelin2014-11-02
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Some reorganization of the code for destruct/induction:Gravatar Hugo Herbelin2014-11-02
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* 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
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Avoid "destruct H" to apply on H itself when H is a section variable.Gravatar Hugo Herbelin2014-10-31
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* Removing the last Evd.diff from Hints.Gravatar Pierre-Marie Pédrot2014-10-27
* Making destruct on idents with maximal implicit arguments working, byGravatar Hugo Herbelin2014-10-27
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* Fixing evars lost in interpretation of eliminator of destruct.Gravatar Hugo Herbelin2014-10-27
* Preventing potential evar leak in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-26
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 21:44:14 +0000