| Age | Commit message (Expand) | Author |
|---|
| 2015-09-09 | Merge remote-tracking branch 'origin/v8.5' into trunk | Hugo Herbelin |
| 2015-09-08 | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin |
| 2015-09-08 | Ensuring that patterns of the form pat/constr move the hypotheses replacing | Hugo Herbelin |
| 2015-09-08 | Short cosmetic changes in tactics.ml. | Hugo Herbelin |
| 2015-09-08 | A bit of documentation of OCaml code for intro_patterns. | Hugo Herbelin |
| 2015-09-08 | New option "Unset Bracketing Last Introduction Pattern" for preserving | Hugo Herbelin |
| 2015-09-08 | Fixing clearing of temporary hypotheses with intro pattern pat/constr. | Hugo Herbelin |
| 2015-09-08 | Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed | Hugo Herbelin |
| 2015-08-22 | Allowing the abstract tactical to clear the environment from unused variables. | Pierre-Marie Pédrot |
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin |
| 2015-05-16 | Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone". | Pierre-Marie Pédrot |
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot |
| 2015-05-04 | Code simplification in Tactics. | Pierre-Marie Pédrot |
| 2015-04-25 | Cleaning some uses of exceptions in tactics. | Pierre-Marie Pédrot |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond |
| 2015-04-23 | Using tclZEROMSG instead of tclZERO in several places. | Pierre-Marie Pédrot |
| 2015-04-10 | Fix #3590 for good this time, by changing the API, change's argument now | Matthieu Sozeau |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-02-27 | Hack so that refine_no_check accepts an argument which is a match on an | Hugo Herbelin |
| 2015-02-26 | Fixing printing of ordinals. | Pierre-Marie Pédrot |
| 2015-02-20 | Fixing error message when H already exists in tactic subexpression eqn:H. | Hugo Herbelin |
| 2015-02-20 | A fix for #3993 (not fully applied term to destruct when eqn is given). | Hugo Herbelin |
| 2015-02-12 | Univs: fix bug #4031: wrong folding of sigma in change. | Matthieu Sozeau |
| 2015-02-11 | Missing space in error message | Matěj Grabovský |
| 2015-02-10 | Fixing #4018 (uncaught exception on non-equality in intros [=]). | Hugo Herbelin |
| 2015-02-10 | More expressive API for tclWITHHOLES. | Pierre-Marie Pédrot |
| 2015-02-10 | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-24 | Removed obsolete option "Legacy Partially Applied Elimination | Hugo Herbelin |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 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 |
