| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-14 | Merge PR#438: Fix V7 syntax in refman. | Maxime Dénès | |
| 2017-03-14 | Merge PR#412: Remove outdated comment from 2002. | Maxime Dénès | |
| 2017-03-14 | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | Maxime Dénès | |
| 2017-03-14 | Merge PR#477: [travis] Basic support for overlays. | Maxime Dénès | |
| 2017-03-14 | Merge PR#473: [ci] Document that sudo: false is slower | Maxime Dénès | |
| 2017-03-14 | Merge PR#464: [META] More fixes | Maxime Dénès | |
| 2017-03-14 | Merge PR#465: Fix #5132: coq_makefile generates incorrect install goal | Maxime Dénès | |
| 2017-03-14 | Fix #5132: coq_makefile generates incorrect install goal | Vadim Zaliva | |
| 2017-03-14 | Merge PR#446: Remove a dead exception catching code. | Maxime Dénès | |
| 2017-03-14 | Fix 3 unused-intro-pattern warnings in stdlib. | Théo Zimmermann | |
| 2017-03-14 | Show unused-intro-pattern warning. | Théo Zimmermann | |
| This warning was shown in CoqIDE but not by coqc. | |||
| 2017-03-14 | [future] Remove unused parameter greedy. | Emilio Jesus Gallego Arias | |
| It was always set to `greedy:true`. | |||
| 2017-03-14 | [library] Refactor state handling. | Emilio Jesus Gallego Arias | |
| This part of state is critical. We refactor it and make it into a record to ease handling. | |||
| 2017-03-14 | [library] Don't recompute path_prefix on unfreeze. | Emilio Jesus Gallego Arias | |
| We instead save the current value. | |||
| 2017-03-13 | [travis] Basic support for overlays. | Emilio Jesus Gallego Arias | |
| We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. | |||
| 2017-03-13 | Remove a dead exception catching code. | Théo Zimmermann | |
| The code was assuming that Proofview.tclFOCUS could raise a CList.IndexOutOfRange exception but this isn't the case. The focusing functions already catch this exception and raises an algebraic exception within the tactic mechanism. | |||
| 2017-03-13 | Merge PR#456: Proposing improvement to the CI targets for local use | Maxime Dénès | |
| 2017-03-12 | Updating core.dbg after ltac moved to plugins directory. | Hugo Herbelin | |
| 2017-03-10 | [travis] Make the git_checkout function more reliable. | Théo Zimmermann | |
| This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). | |||
| 2017-03-10 | [travis] Adding a template file and using it for all targets. | Théo Zimmermann | |
| 2017-03-10 | [travis] Change headband for wider compatibility. | Théo Zimmermann | |
| 2017-03-10 | Improve build of travis target on local machine. | Théo Zimmermann | |
| - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). | |||
| 2017-03-10 | [ci] Document that sudo: false is slower | Tej Chajed | |
| 2017-03-10 | [META] [build] Install dlls to kernel/byterun | Emilio Jesus Gallego Arias | |
| This makes the dll path consistent both in `-local` and non-local Coq install. | |||
| 2017-03-10 | [META] Ltac now a plugin. | Emilio Jesus Gallego Arias | |
| 2017-03-10 | [META] Update version number. | Emilio Jesus Gallego Arias | |
| 2017-03-10 | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals ↵ | Maxime Dénès | |
| correctly as… | |||
| 2017-03-10 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-10 | Merge PR#468: [travis] Fix GeoCoq and move it to allow fail. | Maxime Dénès | |
| 2017-03-09 | Typo doc notations. | Hugo Herbelin | |
| 2017-03-09 | Clarifying doc about interpretation of scopes in notations (#5386). | Hugo Herbelin | |
| 2017-03-09 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-09 | Merge PR#318: Providing a file in the Logic library to work with extensional ↵ | Maxime Dénès | |
| choice | |||
| 2017-03-09 | Micromega: removing a constant preventing micromega to be loaded before Logic.v. | Hugo Herbelin | |
| The constant was useless after 9f56baf which fixed #5073. | |||
| 2017-03-09 | Fixing dependency order of plugins. | Hugo Herbelin | |
| This allows to support static linking of plugins (application to debugging or to when option -natdynlink is "no"). | |||
| 2017-03-07 | Merge PR#452: [ltac] Move dummy plugin to plugins folder. | Maxime Dénès | |
| 2017-03-07 | Fixing Bug 5383 (Hyps Limit) + small refactoring. | Pierre Courtieu | |
| 2017-03-07 | Farewell decl_mode | Enrico Tassi | |
| This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | |||
| 2017-03-07 | Merge PR#453: [travis] Backport trunk's travis support. | Maxime Dénès | |
| 2017-03-07 | Merge PR#436: [ocamlbuild] Update META for the vernac split. | Maxime Dénès | |
| 2017-03-06 | Merge PR#447: [travis] [External CI] fiat-parsers | Maxime Dénès | |
| 2017-03-06 | Merge PR#279: A few lemmas about iff and about orders on positive and Z | Maxime Dénès | |
| 2017-03-03 | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | |
| 2017-03-03 | Strengthening some of the results in ChoiceFacts.v. | Hugo Herbelin | |
| 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. | |||
| 2017-03-03 | Adding explicitly a file to work in the context of propositional extensionality. | Hugo Herbelin | |
| 2017-03-03 | Adding a file providing extensional choice (i.e. choice over setoids). | Hugo Herbelin | |
| Also integrating suggestions from Théo. | |||
| 2017-03-03 | Adding various properties and characterization of the extensional | Hugo Herbelin | |
| axiom of choice (i.e. choice on setoids) and of the axiom selecting representatives in classes of equivalence. Also integrating suggestions from Théo. | |||
| 2017-03-03 | Slightly unifying renaming in ChoiceFacts.v. | Hugo Herbelin | |
| 2017-03-03 | Logic library: Adding a characterization of excluded-middle in term of | Hugo Herbelin | |
| 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). | |||
| 2017-03-03 | Merge PR#273: Tidy stdlib | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |