| Commit message (Expand) | Author | Age |
* | Splitting ML tactics in one function per grammar entry. | Pierre-Marie Pédrot | 2015-01-23 |
* | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot | 2015-01-21 |
* | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | 2015-01-18 |
* | Make native compiler handle universe polymorphic definitions. | Maxime Dénès | 2015-01-18 |
* | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau | 2015-01-18 |
* | Add a (by default deactivated) option to force typeclass resolution to | Matthieu Sozeau | 2015-01-18 |
* | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau | 2015-01-18 |
* | TCs: Properly handle Hint Extern with conclusions of the form _ -> _ | Matthieu Sozeau | 2015-01-13 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Fixing compilation of penultimate commit d08532d. | Hugo Herbelin | 2015-01-08 |
* | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | 2015-01-08 |
* | Fix setoid rewrite. | Arnaud Spiwack | 2015-01-06 |
* | Fixing #3896 (incorrect sigma given to printer). | Hugo Herbelin | 2015-01-03 |
* | A global [gfail] tactic which works like [fail] except that it fails even if ... | Arnaud Spiwack | 2014-12-23 |
* | Remove compatibility layer from Ltac's [fail]. | Arnaud Spiwack | 2014-12-23 |
* | Fix compilation error in some configurations. | Arnaud Spiwack | 2014-12-23 |
* | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack | 2014-12-19 |
* | Fixed bad newlines in output for std output and emacs. | Pierre Courtieu | 2014-12-18 |
* | Fixing bug #3796. | Pierre-Marie Pédrot | 2014-12-17 |
* | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | 2014-12-16 |
* | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
* | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack | 2014-12-12 |
* | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | 2014-12-12 |
* | In discrimination nets, do not index lambdas if they're part of a beta | Matthieu Sozeau | 2014-12-12 |
* | Tentatively more informative report of failure when inferring | Hugo Herbelin | 2014-12-11 |
* | Fix dummy argument use in guess_elim: there are some cases where X_ind | Matthieu Sozeau | 2014-12-10 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | 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-08 |
* | 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-12-07 |
* | For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota | Pierre-Marie Pédrot | 2014-12-02 |
* | More invariants in the code of Rewrite. | Pierre-Marie Pédrot | 2014-12-01 |
* | Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ... | Hugo Herbelin | 2014-11-30 |
* | Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too. | Hugo Herbelin | 2014-11-30 |
* | Reverting the following block of three commits: | Hugo Herbelin | 2014-11-27 |
* | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin | 2014-11-26 |
* | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin | 2014-11-25 |
* | One more word about "simpl f": avoid "simpl f" to be printed "simpl f", | Hugo Herbelin | 2014-11-23 |
* | Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about | Hugo Herbelin | 2014-11-23 |
* | Specific printer of Evar.Set.t for ocamldebug + more information in | Hugo Herbelin | 2014-11-22 |
* | Attempt to organize and document unification flags of setoid rewrite. | Hugo Herbelin | 2014-11-22 |
* | In setoid_rewrite error messages: | 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 |