| Commit message (Expand) | Author | Age |
* | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it" | Hugo Herbelin | 2016-04-27 |
* | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an" | Hugo Herbelin | 2016-04-27 |
* | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ... | Hugo Herbelin | 2016-04-27 |
* | Revert "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin | 2016-04-27 |
* | Temporary hack to compensate missing comma while re-printing tactic | Hugo Herbelin | 2016-04-27 |
* | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels. | Hugo Herbelin | 2016-04-27 |
* | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin | 2016-04-27 |
* | Changing rule for "*" in Operator_Properties so that, iterated, it | Hugo Herbelin | 2016-04-27 |
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-04-09 |
|\ |
|
| * | Added compatibility coercions from Specif.v which were present in Coq 8.4. | Hugo Herbelin | 2016-04-08 |
| * | Add -compat 8.4 econstructor tactics, and tests | Jason Gross | 2016-04-05 |
| * | Fix bug #4656 | Jason Gross | 2016-04-05 |
| * | Update Coq84.v | Jason Gross | 2016-04-04 |
| * | Add compatibility Nonrecursive Elimination Schemes | Jason Gross | 2016-04-04 |
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau | 2016-04-04 |
|\ \ |
|
* \ \ | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-03-30 |
|\ \ \
| | |/
| |/| |
|
| * | | Fix handling of arity of definitional classes. | Matthieu Sozeau | 2016-03-24 |
* | | | Moving Eauto to a simple ML file. | Pierre-Marie Pédrot | 2016-03-06 |
* | | | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot | 2016-03-04 |
* | | | Qcabs : absolute value on normalized rational numbers Qc | Pierre Letouzey | 2016-02-26 |
* | | | Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt) | Pierre Letouzey | 2016-02-26 |
* | | | Qcanon : implement some old suggestions by C. Auger | Pierre Letouzey | 2016-02-26 |
* | | | Moving tauto.ml4 to a proper ML file. | Pierre-Marie Pédrot | 2016-02-23 |
* | | | Moving the Tauto tactic to proper Ltac. | Pierre-Marie Pédrot | 2016-02-22 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-02-21 |
|\| | |
|
| * | | Fixing bug #4582: cannot override notation [ x ]. | Pierre-Marie Pédrot | 2016-02-19 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-29 |
|\| | |
|
| * | | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau | 2016-01-23 |
* | | | 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 |
| * | | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| * | | MMaps: remove it from final 8.5 release, since this new library isn't mature ... | Pierre Letouzey | 2016-01-13 |
* | | | Merge remote-tracking branch 'origin/v8.5' into trunk | Guillaume Melquiond | 2016-01-05 |
|\| | |
|
| * | | Put implicits back as in 8.4. | Matthieu Sozeau | 2015-12-31 |
* | | | Removing auto from the tactic AST. | Pierre-Marie Pédrot | 2015-12-24 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-17 |
|\| | |
|
| * | | Proof using: do not clear unused section hyps automatically | Enrico Tassi | 2015-12-15 |
| * | | Refine tactic now shelves unifiable holes. | Pierre-Marie Pédrot | 2015-12-15 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-15 |
|\| | |
|
| * | | Moved proof_admitted to its own file, named "AdmitAxiom.v". | Maxime Dénès | 2015-12-14 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-11 |
|\| | |
|
| * | | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | 2015-12-10 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-08 |
|\| | |
|
| * | | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
* | | | Fix to previous commit (ClassicalFacts.v). | Hugo Herbelin | 2015-12-05 |
* | | | Adding proofs on the relation between excluded-middle and minimization. | Hugo Herbelin | 2015-12-05 |
* | | | Experimenting removing strong normalization of the mid-statement in tactic cut. | Hugo Herbelin | 2015-12-05 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-11-29 |
|\| | |
|
| * | | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | 2015-11-27 |
* | | | Updating Compat85.v after bd1c97653 on bracketing last or-and | Hugo Herbelin | 2015-11-10 |