aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-14Merge PR#412: Remove outdated comment from 2002.Maxime Dénès
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-03-14Merge PR#477: [travis] Basic support for overlays.Maxime Dénès
2017-03-14Merge PR#473: [ci] Document that sudo: false is slowerMaxime Dénès
2017-03-14Merge PR#464: [META] More fixesMaxime Dénès
2017-03-14Merge 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-13Remove 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-13Merge PR#456: Proposing improvement to the CI targets for local useMaxime Dénès
2017-03-12Updating 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-10Improve 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 slowerTej Chajed
2017-03-10[META] [build] Install dlls to kernel/byterunEmilio 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-10Merge PR#468: [travis] Fix GeoCoq and move it to allow fail.Maxime Dénès
2017-03-09Typo doc notations.Hugo Herbelin
2017-03-09Clarifying 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-09Merge PR#318: Providing a file in the Logic library to work with extensional ↵Maxime Dénès
choice
2017-03-09Micromega: removing a constant preventing micromega to be loaded before Logic.v.Hugo Herbelin
The constant was useless after 9f56baf which fixed #5073.
2017-03-09Fixing 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-07Fixing Bug 5383 (Hyps Limit) + small refactoring.Pierre Courtieu
2017-03-07Merge PR#436: [ocamlbuild] Update META for the vernac split.Maxime Dénès
2017-03-06Merge PR#447: [travis] [External CI] fiat-parsersMaxime Dénès
2017-03-06Merge PR#279: A few lemmas about iff and about orders on positive and ZMaxime Dénès
2017-03-03CHANGES: choice over setoids and prop. ext.Hugo Herbelin
2017-03-03Strengthening 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-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
Also integrating suggestions from Théo.
2017-03-03Adding various properties and characterization of the extensionalHugo 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-03Slightly unifying renaming in ChoiceFacts.v.Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo 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-03Merge PR#273: Tidy stdlibMaxime Dénès
2017-03-03Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Hugo Herbelin
2017-03-03Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Hugo Herbelin
2017-03-03Completing "few lemmas about Zneg" with lemmas also about Zpos.Hugo Herbelin
2017-03-03A 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-03Compatibility of iff wrt not and imp.Hugo Herbelin
This completes the series and cannot hurt.
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-02-27Merge PR#399: Debug by defaultMaxime Dénès
2017-02-27Merge PR#395: Allow hintdb to be parameters in a Ltac definition orMaxime Dénès
Tactic Notation
2017-02-24[travis] [External CI] fiat-parsersEmilio Jesus Gallego Arias
2017-02-24Revert "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-23Fixing #use"include" after vernac is added and ltac is moved to a plugin.Hugo Herbelin
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-22Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:56:30 +0000