| Age | Commit message (Expand) | Author |
|---|
| 2015-01-03 | Fixing #3896 (incorrect sigma given to printer). | Hugo Herbelin |
| 2014-12-23 | 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-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack |
| 2014-12-18 | Fixed bad newlines in output for std output and emacs. | Pierre Courtieu |
| 2014-12-17 | Fixing bug #3796. | Pierre-Marie Pédrot |
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-12-12 | 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-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin |
| 2014-12-10 | Fix dummy argument use in guess_elim: there are some cases where X_ind | Matthieu Sozeau |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 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-12-02 | For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota | Pierre-Marie Pédrot |
| 2014-12-01 | More invariants in the code of Rewrite. | Pierre-Marie Pédrot |
| 2014-11-30 | 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-27 | Reverting the following block of three commits: | Hugo Herbelin |
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin |
| 2014-11-25 | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin |
| 2014-11-23 | 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-22 | 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-21 | Writing Tactics.keep in the new monad. | Pierre-Marie Pédrot |
| 2014-11-20 | Fixing the previous commit. We had to normalize evars first. | Pierre-Marie Pédrot |
| 2014-11-20 | Somehow fixing a side-effect bug in tactics-in-terms. | Pierre-Marie Pédrot |
| 2014-11-20 | Re-removing the Hiddentac module. For some reason it had been reintroduced | Pierre-Marie Pédrot |
| 2014-11-20 | Global.env chasing in Inv. | Pierre-Marie Pédrot |
| 2014-11-20 | Adding locations to tclZEROMSG. | Pierre-Marie Pédrot |
| 2014-11-19 | Print [uconstr]-s in [idtac] messages. | Arnaud Spiwack |
