aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Merge PR#318: Providing a file in the Logic library to work with extensional ↵Gravatar Maxime Dénès2017-03-09
|\ | | | | | | choice
* \ 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | Further highlighting when the correspondence between variants of choice is independent of the domain and codomain of the function, as was done already done in the beginning of the file (suggestion from Jason). Adding some corollaries.
| | * 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
| | | | | | | | | | | | Also integrating suggestions from Théo.
| | * Adding various properties and characterization of the extensionalGravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo.
| | * 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
* | | 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
| | | | | | | | | | | | | | | | | | | | Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
| | * | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| |/ / |/| | | | | | | | This completes the series and cannot hurt.
| | * Formatting references with surrounding brackets in Diaconescu.v.Gravatar Hugo Herbelin2017-03-03
| |/ |/|
* | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
| * Proof clean-up.Gravatar Théo Zimmermann2017-01-30
|/ | | | | | | | | - Do not use induction/elim when not necessary: use destruct or destructive intro-pattern instead. - Do not use heavy automation when lightweight automation is enough. - Prefer shorter proofs when it does not hinder readability. - Do not rely on automatically generated names. - Use bullets.
* 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
| | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
| * 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
| |\ | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics
| | * 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
| |\ \ | | | | | | | | | | | | Was PR#336: Remove v62
| * | | Silence option deprecation warnings in the compat fileGravatar Jason Gross2016-11-04
| | | | | | | | | | | | | | | | Some options are expected to be deprecated
| | * | Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| |/ / | | | | | | | | | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
| | * 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
| | | | | | | | I've messed up with parts of the compatibility files I had to commit.
| * 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
| | | | | | | | | | | | | | | | A file was introduced by mistake in theories/Logic.
* | | | 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
| | | | | | | | | | | | | | | | | | | | if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
| * | | 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
| | |/ | |/| | | | | | | | | | | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
| * | 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
| | | | | | | | | | | | | | | | | | Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
| * | Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
| | | | | | | | | | | | | | | Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
* | | 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-08-25 10:55:53 +0000