| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-14 | [safe-string] plugins/extraction | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-03-14 | [safe-string] ltac/profile_ltac | Emilio Jesus Gallego Arias | |
| No functional change, one extra copy introduced but it seems hard to avoid. | |||
| 2017-03-14 | [safe_string] toplevel/vernac | Emilio Jesus Gallego Arias | |
| No functional changes, only a minor copy on a deprecated output option. | |||
| 2017-03-14 | [safe_string] toplevel/coqloop | Emilio Jesus Gallego Arias | |
| No functional change, even if we could optimize `blanch_utf8_string` a bit more by using `String.init`. | |||
| 2017-03-14 | [safe-string] parsing/cLexer | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-03-14 | [safe_string] interp/dumpglob | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-03-14 | [safe_string] library/nameops | Emilio Jesus Gallego Arias | |
| We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`. | |||
| 2017-03-14 | [safe_string] kernel/cemitcodes | Emilio Jesus Gallego Arias | |
| The `emitcodes` string type was used in both a functional and an imperative way, so we have to handle it with care in order to preserve the previous optimizations and semantics. | |||
| 2017-03-14 | [safe-string] kernel/nativevalues | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-03-14 | [safe_string] kernel/term_typing | Emilio Jesus Gallego Arias | |
| No functional change, we create the new string beforehand and `id_of_string` will become a noop with `-safe-string`. | |||
| 2017-03-14 | [safe-string] lib/miscelanea | Emilio Jesus Gallego Arias | |
| No functional change.js | |||
| 2017-03-14 | [safe-string] lib/cUnix | Emilio Jesus Gallego Arias | |
| No functional change. | |||
| 2017-03-14 | [safe_string] lib/cThread | Emilio Jesus Gallego Arias | |
| No functional changes. | |||
| 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#446: Remove a dead exception catching code. | Maxime Dénès | |
| 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#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 | Fixing Bug 5383 (Hyps Limit) + small refactoring. | Pierre Courtieu | |
| 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 | |
| 2017-03-03 | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |