| Age | Commit message (Expand) | Author |
|---|
| 2016-09-15 | Untangling Tacexpr from lower strata. | Pierre-Marie Pédrot |
| 2016-06-18 | Adding an "as" clause to specialize. | Hugo Herbelin |
| 2016-06-18 | Exporting a generic argument induction_arg. As a consequence, | Hugo Herbelin |
| 2016-06-18 | A cleaning phase around delayed induction arg + exporting force_induction_arg. | Hugo Herbelin |
| 2016-06-18 | Adding eintros to respect the e- prefix policy. | Hugo Herbelin |
| 2016-06-16 | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin |
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot |
| 2016-05-17 | Removing the old refine tactic from the Tactics module. | Pierre-Marie Pédrot |
| 2016-05-17 | Put the "move" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "change" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "specialize_eq" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "generalize dependent" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "cofix" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "*_cast_no_check" tactics in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "exact" family of tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "fix" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "exact_constr" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-16 | Put the "clear" tactic into the monad. | Pierre-Marie Pédrot |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin |
| 2016-04-27 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot |
| 2016-02-15 | Code factorization of tactic "unfold_body". | Pierre-Marie Pédrot |
| 2016-02-15 | More conversion functions in the new tactic API. | Pierre-Marie Pédrot |
| 2016-02-15 | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-14 | Moving is_quantified_hypothesis to new proof engine. | Hugo Herbelin |
| 2016-01-11 | merge | Matej Kosik |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-12-30 | Moving apply_type to new proof engine. | Hugo Herbelin |
| 2015-12-25 | Moving specialize to Proofview.tactic. | Hugo Herbelin |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-11 | Add tactic native_cast_no_check, analog to vm_cast_no_check. | Maxime Dénès |
| 2015-12-05 | Removing redundant versions of generalize. | Hugo Herbelin |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin |
| 2015-10-29 | Monotonizing Tactics.change_arg. | Pierre-Marie Pédrot |
| 2015-10-19 | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot |
| 2015-10-18 | Constraining refine to monotonic functions. | Pierre-Marie Pédrot |
| 2015-09-08 | Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed | Hugo Herbelin |
| 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-01-12 | Update headers. | Maxime Dénès |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-11-22 | Simplifying code of functional induction. | Hugo Herbelin |
| 2014-11-22 | Writing intro_replacing in the new monad. | 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-09 | Removing the unused boolean flag from the move tactic implementation. | Pierre-Marie Pédrot |
