Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR#318: Providing a file in the Logic library to work with extensional ↵ | 2017-03-09 | |
|\ | | | | | | | choice | ||
* | | Micromega: removing a constant preventing micromega to be loaded before Logic.v. | 2017-03-09 | |
| | | | | | | | | The constant was useless after 9f56baf which fixed #5073. | ||
* | | Fixing dependency order of plugins. | 2017-03-09 | |
| | | | | | | | | | | This allows to support static linking of plugins (application to debugging or to when option -natdynlink is "no"). | ||
* | | Fixing Bug 5383 (Hyps Limit) + small refactoring. | 2017-03-07 | |
| | | |||
* | | Merge PR#436: [ocamlbuild] Update META for the vernac split. | 2017-03-07 | |
|\ \ | |||
* \ \ | Merge PR#447: [travis] [External CI] fiat-parsers | 2017-03-06 | |
|\ \ \ | |||
* \ \ \ | Merge PR#279: A few lemmas about iff and about orders on positive and Z | 2017-03-06 | |
|\ \ \ \ | |||
| | | | * | CHANGES: choice over setoids and prop. ext. | 2017-03-03 | |
| | | | | | |||
| | | | * | Strengthening some of the results in ChoiceFacts.v. | 2017-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. | 2017-03-03 | |
| | | | | | |||
| | | | * | Adding a file providing extensional choice (i.e. choice over setoids). | 2017-03-03 | |
| | | | | | | | | | | | | | | | | | | | | Also integrating suggestions from Théo. | ||
| | | | * | Adding various properties and characterization of the extensional | 2017-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. | 2017-03-03 | |
| | | | | | |||
| | | | * | Logic library: Adding a characterization of excluded-middle in term of | 2017-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 stdlib | 2017-03-03 | |
|\ \ \ \ \ | |||
| | * | | | | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z. | 2017-03-03 | |
| | | | | | | |||
| | * | | | | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder. | 2017-03-03 | |
| | | | | | | |||
| | * | | | | Completing "few lemmas about Zneg" with lemmas also about Zpos. | 2017-03-03 | |
| | | | | | | |||
| | * | | | | A couple of other useful properties about compare_cont. | 2017-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. | 2017-03-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | This completes the series and cannot hurt. | ||
| | | | | * | Formatting references with surrounding brackets in Diaconescu.v. | 2017-03-03 | |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge PR#399: Debug by default | 2017-02-27 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | 2017-02-27 | |
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | Tactic Notation | ||
| | | | | * | | [travis] [External CI] fiat-parsers | 2017-02-24 | |
| | | | |/ / | |||
* | | | / / | Revert "Add empty ltac_plugin file for forward compatibility." | 2017-02-24 | |
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only. | ||
* | | | | | Fixing #use"include" after vernac is added and ltac is moved to a plugin. | 2017-02-23 | |
| | | | | | |||
* | | | | | Merge branch 'v8.6' | 2017-02-22 | |
|\ \ \ \ \ | |||
| * \ \ \ \ | Merge branch 'v8.5' into v8.6 | 2017-02-22 | |
| |\ \ \ \ \ | |||
* | | | | | | | [travis] track an 8.7 specific branch of HoTT. | 2017-02-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is required since we merged PR#309: Ltac as a plugin. | ||
* | | | | | | | Merge PR#309: Ltac as a plugin | 2017-02-21 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | Add empty ltac_plugin file for forward compatibility. | 2017-02-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is in preparation for landing of PR#309: Ltac as a plugin | ||
| | | | | * | | | Deprecate -debug flag. | 2017-02-20 | |
| | | | | | | | | |||
* | | | | | | | | Merge PR#189: Remove tabulation support from pretty-printing. | 2017-02-20 | |
|\ \ \ \ \ \ \ \ | |||
| | | | | | | | * | Merge pull request #4 from Zimmi48/patch-1 | 2017-02-20 | |
| | | | | | | | |\ | | | | | | | | | | | | | | | | | | | | | [ocamlbuild] fix small mistakes in descriptions | ||
| | | | | | | | | * | [ocamlbuild] fix small mistakes in descriptions | 2017-02-20 | |
| | | | | | | | |/ | |||
| | | | | | | | * | [ocamlbuild] Update meta for the vernac split. | 2017-02-20 | |
| | | | | | | | | | |||
* | | | | | | | | | Fixing debugger after the split of toplevel into vernac. | 2017-02-19 | |
| |_|_|_|_|_|_|/ |/| | | | | | | | |||
* | | | | | | | | remove obsolete file dev/Makefile.oug | 2017-02-17 | |
| | | | | | | | | |||
| | * | | | | | | Removing spurious folder includes in coq_makefile. | 2017-02-17 | |
| | | | | | | | | |||
| | * | | | | | | Documenting the pluginification of Ltac. | 2017-02-17 | |
| | | | | | | | | |||
| | * | | | | | | Fix .gitignore. | 2017-02-17 | |
| | | | | | | | | |||
| | * | | | | | | Moving the Ltac plugin to a pack-based one. | 2017-02-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements. | ||
| | * | | | | | | Ltac as a plugin. | 2017-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. | ||
| | * | | | | | Fixing #5339 (anomaly with 'pat in record parameters). | 2017-02-16 | |
| | | | | | | | |||
* | | | | | | | Merge PR#403: Split Vernacular Processing from Toplevel | 2017-02-16 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR#431 | 2017-02-16 | |
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | [travis] Add math-comp overlays, update CompCert to official version, add UniMath | ||
| * | | | | | | | | [travis] [External CI] CompCert official 8.6 support + UniMath | 2017-02-15 | |
| | | | | | | | | | |||
| * | | | | | | | | [travis] [External CI] Factor out math-comp installs. | 2017-02-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make math-comp overlays easier, we also start structuring the scripts a bit more. | ||
| | * | | | | | | | Make Obligations see fix_exn | 2017-02-15 | |
| | | | | | | | | | |||
| | * | | | | | | | [stm] Remove unused legacy stm interface. | 2017-02-15 | |
| | | | | | | | | |