aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\
| * Removing unexcepted activation of option "Regular Subst Tactic", sinceGravatar Hugo Herbelin2016-05-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|
| * NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
| * Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
| |\
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\| |
* | | Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
* | | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Gravatar Hugo Herbelin2016-04-27
* | | Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* | | Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* | | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-04-27
* | | Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
* | | Changing rule for "*" in Operator_Properties so that, iterated, itGravatar Hugo Herbelin2016-04-27
| * | Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-04-25
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\| |
| * | Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
| * | Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
| * | Fix bug #4656Gravatar Jason Gross2016-04-05
| * | Update Coq84.vGravatar Jason Gross2016-04-04
| * | Add compatibility Nonrecursive Elimination SchemesGravatar Jason Gross2016-04-04
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |/ / | |/| |
| * | | Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* | | | Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
* | | | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* | | | Qcabs : absolute value on normalized rational numbers QcGravatar Pierre Letouzey2016-02-26
* | | | Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)Gravatar Pierre Letouzey2016-02-26
* | | | Qcanon : implement some old suggestions by C. AugerGravatar Pierre Letouzey2016-02-26
* | | | Moving tauto.ml4 to a proper ML file.Gravatar Pierre-Marie Pédrot2016-02-23
* | | | Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\| | |
| * | | Fixing bug #4582: cannot override notation [ x ].Gravatar Pierre-Marie Pédrot2016-02-19
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| | |
| * | | Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| | |
* | | | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * | | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * | | MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* | | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-05
|\| | |
| * | | Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
| | | * Move compatibility notations to their proper filesGravatar Jason Gross2015-12-29
| | |/ | |/|
* | | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\| |
| * | Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| * | Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\| |
| * | Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14