aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
...
| | * | Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| |/ /
| | * Add Unset Use Unif Heuristics in Compat/Coq85Gravatar Matthieu Sozeau2016-10-22
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * 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.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | 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
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| | |
| * | | Fixing unexpected "noise" introduced in commit 24d5448c.Gravatar Hugo Herbelin2016-10-06
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | 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
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-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
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\| |
| * | 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
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
* | | extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
* | | Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
| * | 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
* | | Add Unset Shrink Abstract/Obligations in Coq85Gravatar Matthieu Sozeau2016-06-27
* | | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18