aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* 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
* 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
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* 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
* Ensuring compatibility when an hypothesis used for destruct isGravatar Hugo Herbelin2014-10-27
* 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
* 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
* Apparently, the former refine was simplifying in hypotheses too.Gravatar Hugo Herbelin2014-10-24
* Addressing report #3279 (inconsistency of behavior of the -> and <-Gravatar Hugo Herbelin2014-10-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 08:06:31 +0000