| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-19 | Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget". | Maxime Dénès | |
| 2017-03-19 | Add a forgotten (?) line to "theories/Logic/vo.itarget". | Matej Kosik | |
| The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that. | |||
| 2017-03-17 | Merge PR#428: Report missing tactic arguments in error message | Maxime Dénès | |
| 2017-03-17 | Merge PR#437: Improve unification debug trace. | Maxime Dénès | |
| 2017-03-17 | Merge PR#445: TACTIC EXTEND now takes an optional level as argument. | Maxime Dénès | |
| 2017-03-17 | Merge PR#442: Allow interactive editing of Coq.Init.Logic | Maxime Dénès | |
| 2017-03-17 | Merge PR#451: Add η principles for sigma types | Maxime Dénès | |
| 2017-03-15 | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | |
| - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390. | |||
| 2017-03-15 | Merge PR#267: Proposal for an update of the recommended style in programming ↵ | Maxime Dénès | |
| Coq. | |||
| 2017-03-14 | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto | Maxime Dénès | |
| 2017-03-14 | Report missing tactic arguments in error message | Tej Chajed | |
| Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344). | |||
| 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#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 |