aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* | Adding an amazing property of Prop.Gravatar Hugo Herbelin2015-11-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-14
| * Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
| * Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \
| | * Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
| | * Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
| |/
| * Add compatibility files (feature 4319)Gravatar Jason Gross2015-09-30
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\|
| * Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
| * Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
| * Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08