| Commit message (Expand) | Author | Age |
* | 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 |
* | Removing a hack which, according to the comment, should not be necessary | Hugo Herbelin | 2014-11-22 |
* | Fix resolve_morphism to build well-scoped terms in case some arguments | Matthieu Sozeau | 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-22 |
* | Writing Tactics.keep in the new monad. | Pierre-Marie Pédrot | 2014-11-21 |
* | Fixing the previous commit. We had to normalize evars first. | Pierre-Marie Pédrot | 2014-11-20 |