| Age | Commit message (Expand) | Author |
|---|
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-13 | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot |
| 2017-06-06 | Remove the Sigma (monotonous state) API. | Maxime Dénès |
| 2017-05-30 | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin |
| 2017-04-25 | Make opaque optional only for tclABSTRACT | Jason Gross |
| 2017-04-25 | Generalize cache_term_by_tactic_then | Jason Gross |
| 2017-04-25 | Add support for transparent abstract (no syntax) | Jason Gross |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot |
| 2017-03-23 | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot |
| 2017-02-14 | Removing most nf_enter in tactics. | Pierre-Marie Pédrot |
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot |
| 2017-02-14 | Hipattern API using EConstr. | Pierre-Marie Pédrot |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot |
| 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 |
