| Commit message (Expand) | Author | Age |
* | 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 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-03 |
|\| |
|
| * | Dead code from August 2014 in apply in. | Hugo Herbelin | 2015-12-02 |
* | | Monotonizing Tactics.change_arg. | Pierre-Marie Pédrot | 2015-10-29 |
* | | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot | 2015-10-19 |
* | | Constraining refine to monotonic functions. | Pierre-Marie Pédrot | 2015-10-18 |
|/ |
|
* | Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed | Hugo Herbelin | 2015-09-08 |
* | Fix #3590 for good this time, by changing the API, change's argument now | Matthieu Sozeau | 2015-04-10 |