aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
* Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Gravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6379: Fix profiling pluginGravatar Maxime Dénès2017-12-14
|\ \ \
* \ \ \ Merge PR #6422: [meta] Minor linking fix.Gravatar Maxime Dénès2017-12-14
|\ \ \ \
* \ \ \ \ Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards com...Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6388: Fix issue #6387Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1108: [stm] Reorganize flagsGravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Gravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma...Gravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | [meta] Minor linking fix.Gravatar Emilio Jesus Gallego Arias2017-12-13
| |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |
| | | | | | | | | | * | | | | Documenting the new options for printing "match".Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | * | | | | Decompiling pattern-matching: mini-removal dead code.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | * | | | | In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | * | | | | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | * | | | | Improving spacing in printing disjunctive patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | * | | | | | | | | Revert "[ci] Temporal workaround for checker non-backwards compatible change."Gravatar Théo Zimmermann2017-12-12
| |_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsGravatar Maxime Dénès2017-12-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | | | | Further clean-up in Reductionops, removing unused lift arguments.Gravatar Maxime Dénès2017-12-12
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6359: Remove most uses of function extensionality in Program.Combin...Gravatar Maxime Dénès2017-12-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6275: [summary] Allow typed projections from global state.Gravatar Maxime Dénès2017-12-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * | | Use msg_info for LtacProfGravatar Jason Gross2017-12-11
| | | | | | | | | | | | | * | | Allow LtacProf tactics to be calledGravatar Jason Gross2017-12-11
* | | | | | | | | | | | | | | | Merge PR #6312: [configure] fix detection of `md5sum`Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * Catch errors while coercing 'and' intro patternsGravatar Tej Chajed2017-12-11
| | | | | | | | | * | | | | | | Fix issue #6387Gravatar Martin Vassor2017-12-11
| |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR #6331: Linter: skip PRs older than the linter.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | |
| | | | | | | | | | * | | | | | | Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Gaëtan Gilbert2017-12-11
| | | | | | | | | * | | | | | | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | * | | | | | | | Restoring filtering of native files passed to `rm` during `make clean`.Gravatar Maxime Dénès2017-12-11
| | | | | | | | | | | | * | | | Add overlay.Gravatar Théo Zimmermann2017-12-11
| | | | | | | | | | | | * | | | Remove deprecated appcontext and corresponding documentation.Gravatar Théo Zimmermann2017-12-11
| | | | | | | | | | | | * | | | Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| | | | | | | | | | | | * | | | Remove deprecated option Dependent Propositions Eliminiation.Gravatar Théo Zimmermann2017-12-11
| |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |
| | | | | | | | | | * | | | | [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | | | | | | * | | | | [stm] Move process_id to Spawned.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6352: [makefile] Address #6291: install more development files.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1150: [stm] Remove all but one use of VtUnknown.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6338: Remove up-to-conversion term matchingGravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 16:28:26 +0000