aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-13Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma...Maxime Dénès
2017-12-13[meta] Minor linking fix.Emilio Jesus Gallego Arias
2017-12-13[econstr] Small cleanup in `vernac/lemmas`Emilio Jesus Gallego Arias
2017-12-13[econstr] Add a couple of new API functions.Emilio Jesus Gallego Arias
2017-12-13[lib] Auxiliary functions in List + fixes.Emilio Jesus Gallego Arias
2017-12-13Circle CI: uses dependencies between external developments.Gaëtan Gilbert
2017-12-13Put bignums, math-classes and corn dependencies in MakefileGaëtan Gilbert
2017-12-13Circle CI: enable TIMED for external developmentsGaëtan Gilbert
2017-12-13Circle CI: use cache for opamGaëtan Gilbert
2017-12-13Circle CI: enable native compiler.Gaëtan Gilbert
2017-12-12Fix #5081 by more fine-grained LtacProf recordingJason Gross
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Near-full implementation of Circle CI.Gaëtan Gilbert
2017-12-12Documenting the new options for printing "match".Hugo Herbelin
2017-12-12Decompiling pattern-matching: mini-removal dead code.Hugo Herbelin
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-12-12Improving spacing in printing disjunctive patterns.Hugo Herbelin
2017-12-12Revert "[ci] Temporal workaround for checker non-backwards compatible change."Théo Zimmermann
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
2017-12-12Further clean-up in Reductionops, removing unused lift arguments.Maxime 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-11Use msg_info for LtacProfJason Gross
2017-12-11Allow LtacProf tactics to be calledJason Gross
2017-12-11Merge PR #6312: [configure] fix detection of `md5sum`Maxime Dénès
2017-12-11CI: poc Circleci configurationArnaud Spiwack
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
2017-12-11Fix issue #6387Martin Vassor
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-11Add overlay.Théo Zimmermann
2017-12-11Remove deprecated appcontext and corresponding documentation.Théo Zimmermann
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
2017-12-11Remove deprecated option Dependent Propositions Eliminiation.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 01:01:01 +0000