aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".Gravatar Pierre-Marie Pédrot2015-05-16
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Code simplification in Tactics.Gravatar Pierre-Marie Pédrot2015-05-04
* Cleaning some uses of exceptions in tactics.Gravatar Pierre-Marie Pédrot2015-04-25
* 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
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
* Fixing error message when H already exists in tactic subexpression eqn:H.Gravatar Hugo Herbelin2015-02-20
* A fix for #3993 (not fully applied term to destruct when eqn is given).Gravatar Hugo Herbelin2015-02-20
* Univs: fix bug #4031: wrong folding of sigma in change.Gravatar Matthieu Sozeau2015-02-12
* Missing space in error messageGravatar Matěj Grabovský2015-02-11
* Fixing #4018 (uncaught exception on non-equality in intros [=]).Gravatar Hugo Herbelin2015-02-10
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Removed obsolete option "Legacy Partially Applied EliminationGravatar Hugo Herbelin2015-01-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
* This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Gravatar Hugo Herbelin2014-12-08
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Step 4 : atomize_thenGravatar Hugo Herbelin2014-12-07
* Step 2Gravatar Hugo Herbelin2014-12-07
* Step 1Gravatar Hugo Herbelin2014-12-07
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutGravatar Hugo Herbelin2014-11-23
* Further simplifying functional induction.Gravatar Hugo Herbelin2014-11-22
* Simplifying code of functional induction.Gravatar Hugo Herbelin2014-11-22
* Not using an (arbitrary) pivot anymore for re-introduction ofGravatar Hugo Herbelin2014-11-22
* New simplification of code for generalizing hypotheses in destruct.Gravatar Hugo Herbelin2014-11-22
* Removing a hack which, according to the comment, should not be necessaryGravatar Hugo Herbelin2014-11-22
* Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing intro_replacing in the new monad.Gravatar Pierre-Marie Pédrot2014-11-22
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* 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
* Removing the unused boolean flag from the move tactic implementation.Gravatar Pierre-Marie Pédrot2014-11-09
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 03:07:29 +0000