| Age | Commit message (Expand) | Author |
|---|
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack |
| 2014-12-10 | Fix dummy argument use in guess_elim: there are some cases where X_ind | Matthieu Sozeau |
| 2014-12-08 | This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e. | Hugo Herbelin |
| 2014-12-08 | Constructor tactics backtracking is done using [Tacticals.New] rather than [P... | Arnaud Spiwack |
| 2014-12-07 | Step 4 : atomize_then | Hugo Herbelin |
| 2014-12-07 | Step 2 | Hugo Herbelin |
| 2014-12-07 | Step 1 | Hugo Herbelin |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-12-07 | Exporting store of goals so that new_evar in convert, intro, etc. can | Hugo Herbelin |
| 2014-11-23 | Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about | Hugo Herbelin |
| 2014-11-22 | Further simplifying functional induction. | Hugo Herbelin |
| 2014-11-22 | Simplifying code of functional induction. | Hugo Herbelin |
| 2014-11-22 | Not using an (arbitrary) pivot anymore for re-introduction of | Hugo Herbelin |
| 2014-11-22 | New simplification of code for generalizing hypotheses in destruct. | Hugo Herbelin |
| 2014-11-22 | Removing a hack which, according to the comment, should not be necessary | Hugo Herbelin |
| 2014-11-22 | Enforcing the non-normalization of evars in Tactics.get_next_hyp_position. | Pierre-Marie Pédrot |
| 2014-11-22 | Writing intro_replacing in the new monad. | Pierre-Marie Pédrot |
| 2014-11-22 | Removing useless flag of the historical move tactic. | Pierre-Marie Pédrot |
| 2014-11-21 | Writing Tactics.keep in the new monad. | Pierre-Marie Pédrot |
| 2014-11-16 | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin |
| 2014-11-14 | Preserving the good effect of 014e5ac92a on not leaving dangling local | Hugo Herbelin |
| 2014-11-13 | Removing yet another source of remaining local definitions. | Hugo Herbelin |
| 2014-11-11 | Renouncing to check only at the end of the call to "apply in" the | Hugo Herbelin |
| 2014-11-09 | Removing the unused boolean flag from the move tactic implementation. | Pierre-Marie Pédrot |
| 2014-11-08 | Compatibility with 8.4 in the heuristic used to build the induction | Hugo Herbelin |
| 2014-11-07 | Granting #3717 (more informative error message on missing arguments for funct... | Hugo Herbelin |
| 2014-11-06 | Restoring clear_flag (thanks a lot to jonikelee to notice it). | Hugo Herbelin |
| 2014-11-06 | Optimizing when to clear generalized hypotheses in destruct. | Hugo Herbelin |
| 2014-11-06 | Dependency bug in using eqn for destruct. | Hugo Herbelin |
| 2014-11-05 | Writing the raw introduction tactic in the new monad. | Pierre-Marie Pédrot |
| 2014-11-03 | Writing rename_hyps in the new monad. | Pierre-Marie Pédrot |
| 2014-11-03 | Subtle swap of lines to preserve VarInstance src field before checking | Hugo Herbelin |
| 2014-11-03 | Fix to 844431761 on improving elimination with indices, getting rid of | Hugo Herbelin |
| 2014-11-02 | Saving some nf_evars in the code of destruct/induction. | Hugo Herbelin |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin |
| 2014-11-02 | Some reorganization of the code for destruct/induction: | Hugo Herbelin |
| 2014-11-02 | Fixing 1177da327 (reorganization of the test for generic selection of | Hugo Herbelin |
| 2014-10-31 | Reorganization of the test for generic selection of occurrences in | Hugo Herbelin |
| 2014-10-31 | Enlarge the cases where the like first selection is used in destruct. | Hugo Herbelin |
| 2014-10-31 | Avoid "destruct H" to apply on H itself when H is a section variable. | Hugo Herbelin |
| 2014-10-27 | Cleaning and documenting Clenv.make_evar_clause | Pierre-Marie Pédrot |
| 2014-10-27 | Ensuring compatibility when an hypothesis used for destruct is | Hugo Herbelin |
| 2014-10-26 | Fixing destruct/induction with a using clause on a non-inductive type, | Hugo Herbelin |
| 2014-10-26 | Dead code + typo. | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-24 | Change reduction_of_red_expr to return an e_reduction_function returning | Matthieu Sozeau |
| 2014-10-24 | Apparently, the former refine was simplifying in hypotheses too. | Hugo Herbelin |
| 2014-10-24 | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin |
