aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-13Merge PR #1108: [stm] Reorganize flagsMaxime Dénès
2017-12-13Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Maxime Dénès
2017-12-13Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Maxime Dénès
2017-12-13Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma...Maxime Dénès
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
2017-12-12Merge PR #6359: Remove most uses of function extensionality in Program.Combin...Maxime Dénès
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
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-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Restoring filtering of native files passed to `rm` during `make clean`.Maxime Dénès
2017-12-11[flags] [stm] Reorganize flags.Emilio Jesus Gallego Arias
2017-12-11[stm] Move process_id to Spawned.Emilio Jesus Gallego Arias
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-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-12-10Merge PR #6370: [ci] Temporal workaround for checker non-backwards compatible...Maxime Dénès
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
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
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
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