| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2017-03-03 | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z. | Hugo Herbelin | |
| 2017-03-03 | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder. | Hugo Herbelin | |
| 2017-03-03 | Completing "few lemmas about Zneg" with lemmas also about Zpos. | Hugo Herbelin | |
| 2017-03-03 | A couple of other useful properties about compare_cont. | Hugo Herbelin | |
| Don't know if compare_cont is very useful to use, but, at least, these extensions make sense. | |||
| 2017-03-03 | Compatibility of iff wrt not and imp. | Hugo Herbelin | |
| This completes the series and cannot hurt. | |||
| 2017-03-03 | Formatting references with surrounding brackets in Diaconescu.v. | Hugo Herbelin | |
| 2017-03-03 | [ltac] Move dummy plugin to plugins folder. | Emilio Jesus Gallego Arias | |
| This is needed to fix `Declare ML Module "ltac_plugin". | |||
| 2017-03-02 | [travis] Backport trunk's travis support. | Emilio Jesus Gallego Arias | |
| 2017-03-01 | Add η principles for sigma types | Jason Gross | |
| 2017-03-01 | Remove some trailing whitespace in Init/Specif.v | Jason Gross | |
| 2017-02-27 | Merge PR#399: Debug by default | Maxime Dénès | |
| 2017-02-27 | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | Maxime Dénès | |
| Tactic Notation | |||
| 2017-02-27 | Do not recompute twice the whnf of terms in conversion. | Pierre-Marie Pédrot | |
| This performance bug was introduced 9 years ago in a8b0345, where the responsibility of normalizing the term went from ccnv to eqappr in Reduction. As a result, all recursive calls to eqappr that were preemptively reducing the term ended up calling whd_stack twice, once by themselves, and once in the subsequent call to eqappr. This caused an important slowdown for conversion-intensive proofs, as the whd_stack calls CClosure.zip to perfom in-place term sharing, leading to useless huge re-allocations and repetitive write barriers. Now that eqappr always head-normalizes the term beforehand, we simply don't call whd_stack anymore when jumping to eqappr. | |||
| 2017-02-24 | [travis] [External CI] fiat-parsers | Emilio Jesus Gallego Arias | |
| 2017-02-24 | TACTIC EXTEND now takes an optional level as argument. | Maxime Dénès | |
| The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ... | |||
| 2017-02-24 | Revert "Add empty ltac_plugin file for forward compatibility." | Maxime Dénès | |
| This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only. | |||
| 2017-02-24 | Simplifying the proof of NoRetractToModalProposition.paradox in | Hugo Herbelin | |
| Hurkens.v by dropping the artificial need for monad laws. Tactic eauto decided to be dependent on the laws but there is a shorter proof without them. [Interestingly, eauto is not able to find the short proof. This is a situation of the form subgoal 1: H : ?A |- P x subgoal 2: H : M ?A |- M (forall x, P x) where addressing the second subgoal would find the right instance of ?A, but this instance is too hard to find by addressing first the first subgoal.] | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |