aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-09[summary] Allow typed projections from global state + rework of internals.Emilio Jesus Gallego Arias
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
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
2017-12-08Revert "CI: poc Circleci configuration"Arnaud Spiwack
2017-12-08CI: poc Circleci configurationArnaud Spiwack
2017-12-08[makefile] Address #6291: install more development files.Emilio Jesus Gallego Arias
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
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
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
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
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
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
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
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-12-05use preference for ocamlfindPaul 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
2017-12-05Merge PR #6287: Add merlin to default.nixMaxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès