| Commit message (Expand) | Author | Age |
* | 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 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-13 |
|\ |
|
| * | Fixing a try with in apply that has become too weak in 8.5. | Hugo Herbelin | 2016-06-11 |
* | | Fixing #4787 (Unset Bracketing Last Introduction Pattern not working). | Hugo Herbelin | 2016-06-07 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-01 |
|\| |
|
* | | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
| * | Fix bug #4746: Anomaly: Evar ?X10 was not declared. | Pierre-Marie Pédrot | 2016-05-29 |
* | | Removing some compatibility layers in Tactics. | 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 |
* | | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-04 |
|\| |
|
| * | Fix bug #4707: clearbody much slower in 8.5pl1. | Pierre-Marie Pédrot | 2016-05-03 |
* | | 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 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-04-09 |
|\| |
|
| * | Fixing the "No applicable tactic" non informative error message | Hugo Herbelin | 2016-04-03 |
* | | Moving Refine to its proper module. | Pierre-Marie Pédrot | 2016-03-20 |
* | | Making Proofview independent of Logic. | Pierre-Marie Pédrot | 2016-03-20 |
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | 2016-02-15 |
|\ \ |
|
* | | | Using monotonic types for conversion functions. | 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-02-15 |
* | | | Renaming functions in Typing to stick to the standard e_* scheme. | Pierre-Marie Pédrot | 2016-02-15 |
* | | | Monotonizing the Evarutil module. | Pierre-Marie Pédrot | 2016-02-15 |
| * | | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
|/ / |
|
* | | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns. | Hugo Herbelin | 2016-01-22 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| |
|
* | | Stronger invariants on the use of the introduction pattern (pat1,...,patn). | Hugo Herbelin | 2016-01-21 |
* | | Fixing a bug with introduction patterns over inductive types containing let-ins. | Hugo Herbelin | 2016-02-18 |
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| * | Fix bug #4420: check_types was losing universe constraints. | Matthieu Sozeau | 2016-01-19 |
* | | Moving is_quantified_hypothesis to new proof engine. | Hugo Herbelin | 2016-01-14 |
* | | Update in the documentation of parts of the code of destruct/induction. | Hugo Herbelin | 2016-01-14 |
* | | merge | Matej Kosik | 2016-01-11 |
|\ \ |
|
| * | | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
* | | | Remove useless rec flags. | Guillaume Melquiond | 2016-01-02 |