| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | | | | | | | | | | | | * | | | | Put bignums, math-classes and corn dependencies in Makefile |  Gaëtan Gilbert | 2017-12-13 | |
| | | | | | | | | | | | | | | | | | | | | | * | | | | Circle CI: enable TIMED for external developments | Gaëtan Gilbert | 2017-12-13 | |
| | | | | | | | | | | | | | | | | | | | | | * | | | | Circle CI: use cache for opam | Gaëtan Gilbert | 2017-12-13 | |
| | | | | | | | | | | | | | | | | | | | | | * | | | | Circle CI: enable native compiler. | Gaëtan Gilbert | 2017-12-13 | |
| | | | | | | | | | | | | | | | | | * | | | | | | | | Fix #5081 by more fine-grained LtacProf recording |  Jason Gross | 2017-12-12 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | [econstr] Cleanup in `vernac/classes.ml`. |  Emilio Jesus Gallego Arias | 2017-12-13 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | Near-full implementation of Circle CI. | Gaëtan Gilbert | 2017-12-12 | |
| | | | | | | | | | | * | | | | | | | | | | | | | Documenting the new options for printing "match". |  Hugo Herbelin | 2017-12-12 | |
| | | | | | | | | | | * | | | | | | | | | | | | | Decompiling pattern-matching: mini-removal dead code. | Hugo Herbelin | 2017-12-12 | |
| | | | | | | | | | | * | | | | | | | | | | | | | In printing, factorizing "match" clauses with same right-hand side. | Hugo Herbelin | 2017-12-12 | |
| | | | | | | | | | | * | | | | | | | | | | | | | Removing cumbersome location in multiple patterns. | Hugo Herbelin | 2017-12-12 | |
| | | | | | | | | | | * | | | | | | | | | | | | | Improving spacing in printing disjunctive patterns. | Hugo Herbelin | 2017-12-12 | |
| | | | | | | * | | | | | | | | | | | | | | | | | Revert "[ci] Temporal workaround for checker non-backwards compatible change." |  Théo Zimmermann | 2017-12-12 | |
| | |_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts |  Maxime Dénès | 2017-12-12 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | | | | | Further clean-up in Reductionops, removing unused lift arguments. | Maxime Dénès | 2017-12-12 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | Merge PR #6359: Remove most uses of function extensionality in Program.Combin... | Maxime Dénès | 2017-12-12 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6275: [summary] Allow typed projections from global state. | Maxime Dénès | 2017-12-12 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | * | | | | | | | | | | | Use msg_info for LtacProf | Jason Gross | 2017-12-11 | |
| | | | | | | | | | | | | | * | | | | | | | | | | | Allow LtacProf tactics to be called | Jason Gross | 2017-12-11 | |
| | | | | | | | | | | | | | | |_|_|/ / / / / / / | | | | | | | | | | | | | |/| | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6312: [configure] fix detection of `md5sum` | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | CI: poc Circleci configuration |  Arnaud Spiwack | 2017-12-11 | |
| | | | | | | | | | | | | | | | * | | | | | | | | Catch errors while coercing 'and' intro patterns |  Tej Chajed | 2017-12-11 | |
| | | | | | | | | | | | | | | | | |_|_|/ / / / | | | | | | | | | | | | | | | |/| | | | | | | ||||
| | | | | | | | | | * | | | | | / | | | | | | | Fix issue #6387 |  Martin Vassor | 2017-12-11 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #6331: Linter: skip PRs older than the linter. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153 | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | | | | | | | Fix 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-11 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | Restoring filtering of native files passed to `rm` during `make clean`. | Maxime Dénès | 2017-12-11 | |
| | | | | | | | | | | | | * | | | | | | | | | | Add overlay. | Théo Zimmermann | 2017-12-11 | |
| | | | | | | | | | | | | * | | | | | | | | | | Remove deprecated appcontext and corresponding documentation. | Théo Zimmermann | 2017-12-11 | |
| | | | | | | | | | | | | * | | | | | | | | | | Remove deprecated option Tactic Compat Context. | Théo Zimmermann | 2017-12-11 | |
| | | | | | | | | | | | | * | | | | | | | | | | Remove 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-11 | |
| | |_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | Merge PR #6368: [api] Remove yet another type alias. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6352: [makefile] Address #6291: install more development files. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1150: [stm] Remove all but one use of VtUnknown. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6338: Remove up-to-conversion term matching | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind) | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6363: [META] Some dependency fixes. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6351: Fix a copy-paste error in ci-ltac2. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6346: [ci] CoLoR has moved to github | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6340: [default.nix] Add ocpIndent and ocp-index. | Maxime Dénès | 2017-12-11 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | | Axiom-free proof of eta expansion. |  Jasper Hugunin | 2017-12-11 | |
| | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | [make] remove unneeded generated file "tolink.ml" | Emilio Jesus Gallego Arias | 2017-12-10 | |
| | | | | | | | | | | | | | | | | | | | | | * | | | | | | | | | [build] Remove coqmktop in favor of ocamlfind. | Emilio Jesus Gallego Arias | 2017-12-10 | |
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6370: [ci] Temporal workaround for checker non-backwards compatible... | Maxime Dénès | 2017-12-10 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |