aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* 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
* | | 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
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\| |
| * | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\| |
| * | Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | | Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
* | | Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
* | | Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\| |
| * | Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* | | Updating Compat85.v after bd1c97653 on bracketing last or-andGravatar Hugo Herbelin2015-11-10