| Commit message (Expand) | Author | Age |
* | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
* | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot | 2017-06-13 |
* | Remove the Sigma (monotonous state) API. | Maxime Dénès | 2017-06-06 |
* | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin | 2017-05-30 |
* | 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-25 |
* | Merge branch 'master' into econstr | Pierre-Marie Pédrot | 2017-04-07 |
|\ |
|
| * | Ensuring static invariants about handling of pending evars in Pretyping. | Pierre-Marie Pédrot | 2017-03-23 |
* | | 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 | 2017-02-14 |
|/ |
|
* | Untangling Tacexpr from lower strata. | Pierre-Marie Pédrot | 2016-09-15 |
* | 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-18 |
* | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin | 2016-06-16 |
* | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 |
* | 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-17 |
* | 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-05-16 |
* | 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-04-27 |
* | Moving Refine to its proper module. | Pierre-Marie Pédrot | 2016-03-20 |
* | 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-02-15 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\ |
|
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | Moving is_quantified_hypothesis to new proof engine. | Hugo Herbelin | 2016-01-14 |
* | | merge | Matej Kosik | 2016-01-11 |
|\ \ |
|
| * | | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
* | | | Moving apply_type to new proof engine. | Hugo Herbelin | 2015-12-30 |
* | | | Moving specialize to Proofview.tactic. | Hugo Herbelin | 2015-12-25 |
|/ / |
|
* | | 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-11 |
* | | Removing redundant versions of generalize. | Hugo Herbelin | 2015-12-05 |