aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge PR#318: Providing a file in the Logic library to work with extensional ...Gravatar Maxime Dénès2017-03-09
|\
* \ Merge PR#279: A few lemmas about iff and about orders on positive and ZGravatar Maxime Dénès2017-03-06
|\ \
| | * Strengthening some of the results in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | * Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
| | * Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
| | * Adding various properties and characterization of the extensionalGravatar Hugo Herbelin2017-03-03
| | * Slightly unifying renaming in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | * Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
* | | Merge PR#273: Tidy stdlibGravatar Maxime Dénès2017-03-03
|\ \ \
| | * | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Gravatar Hugo Herbelin2017-03-03
| | * | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Gravatar Hugo Herbelin2017-03-03
| | * | Completing "few lemmas about Zneg" with lemmas also about Zpos.Gravatar Hugo Herbelin2017-03-03
| | * | A couple of other useful properties about compare_cont.Gravatar Hugo Herbelin2017-03-03
| | * | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| |/ / |/| |
| | * Formatting references with surrounding brackets in Diaconescu.v.Gravatar Hugo Herbelin2017-03-03
| |/ |/|
* | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| * Proof clean-up.Gravatar Théo Zimmermann2017-01-30
|/
* Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * 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
| |/
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 15:08:26 +0000