aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-20[misc] Remove warnings about String.setEmilio Jesus Gallego Arias
The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings.
2017-03-14[safe-string] Enable -safe-string !Emilio Jesus Gallego Arias
We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed.
2017-03-14[safe-string] toolsEmilio Jesus Gallego Arias
No functional changes.
2017-03-14[safe-string] ideEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe-string] plugins/extractionEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe-string] ltac/profile_ltacEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe_string] toplevel/vernacEmilio Jesus Gallego Arias
No functional changes, only a minor copy on a deprecated output option.
2017-03-14[safe_string] toplevel/coqloopEmilio 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/cLexerEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] library/nameopsEmilio 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/cemitcodesEmilio 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/nativevaluesEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] kernel/term_typingEmilio 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/miscelaneaEmilio Jesus Gallego Arias
No functional change.js
2017-03-14[safe-string] lib/cUnixEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] lib/cThreadEmilio Jesus Gallego Arias
No functional changes.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 15:17:43 +0000