aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* | | 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
* | | Remove unneded hints in NZGcdGravatar Matthieu Sozeau2016-06-16
* | | setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
* | | Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16