aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-11Merge PR #6312: [configure] fix detection of `md5sum`Maxime Dénès
2017-12-11Merge PR #6331: Linter: skip PRs older than the linter.Maxime Dénès
2017-12-11Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153Maxime Dénès
2017-12-11Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Maxime Dénès
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6352: [makefile] Address #6291: install more development files.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-11Merge PR #1150: [stm] Remove all but one use of VtUnknown.Maxime Dénès
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-11Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)Maxime Dénès
2017-12-11Merge PR #6363: [META] Some dependency fixes.Maxime Dénès
2017-12-11Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Maxime Dénès
2017-12-11Merge PR #6351: Fix a copy-paste error in ci-ltac2.Maxime Dénès
2017-12-11Merge PR #6346: [ci] CoLoR has moved to githubMaxime Dénès
2017-12-11Merge PR #6340: [default.nix] Add ocpIndent and ocp-index.Maxime Dénès
2017-12-10Merge PR #6370: [ci] Temporal workaround for checker non-backwards ↵Maxime Dénès
compatible change.
2017-12-10[ci] Temporal workaround for checker non-backwards compatible change.Emilio Jesus Gallego Arias
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[META] Some dependency fixes.Emilio Jesus Gallego Arias
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
2017-12-09Remove up-to-conversion matching functions.Pierre-Marie Pédrot
They were not used anymore since the previous patches.
2017-12-09[ci] Download ci-sf archives into the proper CI build dir.Emilio Jesus Gallego Arias
Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
2017-12-08Revert "CI: poc Circleci configuration"Arnaud Spiwack
Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
2017-12-08CI: poc Circleci configurationArnaud Spiwack
2017-12-08[makefile] Address #6291: install more development files.Emilio Jesus Gallego Arias
As noted in the bug #6291, `.cmx` files are not installed in the coqlib, which yields the warning: ``` Warning 58: no cmx file was found in path for module Sorts, and its interface was not compiled with -opaque ``` We thus install the `cmx` files to fix this problem, and also install the `.o` files for plugins' `.o` to support linking the plugins statically. This closes #5099 and #6291.
2017-12-08Fix a copy-paste error in ci-ltac2.Théo Zimmermann
2017-12-08Merge PR #6334: Remove dead code in ReductionopsMaxime Dénès
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-08Merge PR #6224: Add alienclean target to remove compilation products with no ↵Maxime Dénès
source.
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
Closes #6194 .
2017-12-07Merge PR #6267: Fix PR merge script.Maxime Dénès
2017-12-07[default.nix] Add ocpIndent and ocp-index.Maxime Dénès
2017-12-07Getting rid of pf_matches in Hipattern.Pierre-Marie Pédrot
Funnily enough, the old code is completely bogus. It succeeds in early files of the prelude just because the heterogeneous equality has not been required. This raises an exception which is not the same one as if we tried to rewrite with the identity type first. The only user, the inversion tactic, was actually only relying on Logic.eq and was furthermore not even using the convertibility algorithm. We just perform a syntactic match now.
2017-12-07Merge PR #6290: Rename update to set, Fixes #6196Maxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ↵Maxime Dénès
to use among several of them
2017-12-07Merge PR #6142: Single quotes break on WindowsMaxime Dénès
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07[configure] fix spelling mistakeVincent Laporte
2017-12-07Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Maxime Dénès
2017-12-07Merge PR #6321: Use preference for ocamlfind in configureMaxime Dénès
2017-12-07Merge PR #6316: Correct typoMaxime Dénès
2017-12-07Merge PR #6309: [default.nix] needs ncurses for the test-suiteMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-06Getting rid of pf_is_matching in Funind.Pierre-Marie Pédrot
2017-12-06Getting rid of the Update constructor in Reductionops.Pierre-Marie Pédrot
This was dead code, probably due to the fact it was once shared with the kernel stack type.
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
It was actually not used. The only place generating one was easily writable without it.
2017-12-06Overlay for Equations.Gaëtan Gilbert
2017-12-06Linter: skip PRs older than the linter.Gaëtan Gilbert
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 02:49:57 +0000