aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Maxime Dénès2017-06-01
* Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
|\
* | Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
| * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-12-26
* | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \
| * | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
* | | Merge remote-tracking branch 'github/pr/336' into v8.6Gravatar Maxime Dénès2016-11-04
|\ \ \
* | | | Silence option deprecation warnings in the compat fileGravatar Jason Gross2016-11-04
| * | | Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
|/ / /
| * / Add Unset Use Unif Heuristics in Compat/Coq85Gravatar Matthieu Sozeau2016-10-22
|/ /
* | Fix previous commit.Gravatar Pierre-Marie Pédrot2016-10-17
* | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \
* \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ | | |/ | |/|
* | | Little addition to 6eede071 for consistency of style in OrdersFacts.v.Gravatar Hugo Herbelin2016-10-12
* | | Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
* | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| * | Remove if_then_else. Use tryif instead.Gravatar Théo Zimmermann2016-10-03
* | | More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| |/ |/|
* | ZDivEucl: notations in different scope to avoid a warningGravatar Pierre Letouzey2016-09-28
* | Remove spaces from around list notationsGravatar Jason Gross2016-09-26
* | Remove spaces from around vector notationsGravatar Jason Gross2016-09-26
* | Unbreak Ltac [ | .. | ] notation in -compat 8.5Gravatar Jason Gross2016-09-26
* | Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
* | Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
* | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | Refolding: disable in 8.4 compat file, documentGravatar Matthieu Sozeau2016-09-12
* | no-refold patchGravatar Paul Steckler2016-09-09
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
|\|
| * Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
* | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\ \
* \ \ Merge remote-tracking branch 'github/bug4978' into v8.6Gravatar Matthieu Sozeau2016-08-18
|\ \ \
* | | | Fix an occurrence of deprecated eqn syntax in stdlib.Gravatar Maxime Dénès2016-08-18
| * | | Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
|/ / /
* | | Replacing deprecated Implicit Arguments in prelude.Gravatar Maxime Dénès2016-07-18
* | | Remove the swap tactic from the prelude.Gravatar Maxime Dénès2016-07-18
* | | Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
| | * Typo.Gravatar Hugo Herbelin2016-07-13
* | | Typo in a comment of stdlib.Gravatar Hugo Herbelin2016-07-08
| * | Program: Move ProofIrrelevance to Subset.vGravatar Matthieu Sozeau2016-07-08
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \ \ | |/ / |/| / | |/
| * Merge remote-tracking branch 'github/pr/199' into v8.5Gravatar Maxime Dénès2016-07-06
| |\
* | | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| * | Move option_map notation upGravatar Jason Gross2016-07-05
| * | Restore option_map in FMapFactsGravatar Jason Gross2016-07-05
| | * Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
* | | Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28