aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-09[lib] Convenience function for `Dyn.Easy`Emilio Jesus Gallego Arias
2017-12-09Remove up-to-conversion matching functions.Pierre-Marie Pédrot
They were not used anymore since the previous patches.
2017-12-09Remove most uses of function extensionality in Program.CombinatorsJasper Hugunin
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-08Adapt to removal of match_appsubterm.Théo Zimmermann
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-06Additional rewrite lemmas on Ensembles, in Powerset_factsJoachim Breitner
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-06issue deprecation warning for "Ocaml"Paul Steckler
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].
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
This fixes #6286 as suggested by PMP. See details of discussion at #6286.
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-12-05use preference for ocamlfindPaul Steckler
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-05Don't Add LoadPath on CoqIDE startup, #6153Paul Steckler
2017-12-05Correct typoMartin Vassor
2017-12-05[default.nix] explain ncurses dependencyVincent Laporte
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-05[configure] adds a `select_command` functionVincent Laporte
2017-12-05Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.Maxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6300: Clarify operation of sequences, fixes #6095Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162Maxime Dénès
2017-12-05Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 17:34:26 +0000