| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-11 | [native_compute] Delay computations with toplevel match | Maxime Dénès | |
| This is an easy improvement on examples like: Fixpoint zero (n : nat) := match n with | O => O | S p => zero p + zero p end. Definition foo := if true then zero 100 else 0. Eval native_compute in if true then 0 else foo. I didn't add a test case, because our current testing infrastructure is too fragile for that. | |||
| 2018-06-11 | [ci] GeoCoq now depends on math-comp's ssralg. | Emilio Jesus Gallego Arias | |
| 2018-06-10 | Tweak printing boxes for unicode binders | Ralf Jung | |
| 2018-06-10 | [VM] Remove projection names from structured constants. | Maxime Dénès | |
| It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations. | |||
| 2018-06-10 | Fixing #7700 (section variables bound to abbreviations were not found). | Hugo Herbelin | |
| Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned. | |||
| 2018-06-10 | [lib] Fix wrong deprecation comment. | Emilio Jesus Gallego Arias | |
| 2018-06-09 | Merge PR #7691: Fixing spelling of statment/statement in two API types | Pierre-Marie Pédrot | |
| 2018-06-09 | [merge script] Check if the CI that was run is outdated. | Théo Zimmermann | |
| [ci skip] | |||
| 2018-06-09 | Merge PR #7515: gitlab: build sphinx doc in separate job | Emilio Jesus Gallego Arias | |
| 2018-06-09 | Merge PR #7642: Gitlab: retry failed jobs once | Emilio Jesus Gallego Arias | |
| 2018-06-08 | gitlab: build sphinx doc in separate job | Gaëtan Gilbert | |
| 2018-06-08 | Existing Class noop when already a class + warning. | Gaëtan Gilbert | |
| Fix #5012. | |||
| 2018-06-08 | Merge PR #7739: add test for #7595 | Gaëtan Gilbert | |
| 2018-06-08 | Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ↵ | Théo Zimmermann | |
| info | |||
| 2018-06-08 | Add a bit of doc to EConstr.decompose_lam* | Gaëtan Gilbert | |
| 2018-06-08 | [doc] Disable smartquotes conversion | Clément Pit-Claudel | |
| Closes GH-7742. | |||
| 2018-06-08 | dev/doc/univpoly.{txt => md}, split off primitive projection info | Gaëtan Gilbert | |
| 2018-06-08 | Gitlab: retry failed "build" jobs once | Gaëtan Gilbert | |
| 2018-06-08 | Merge PR #7417: Micromega clean-up | Théo Zimmermann | |
| 2018-06-08 | Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies. | Gaëtan Gilbert | |
| 2018-06-07 | Micromega clean-up | Maxime Dénès | |
| We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication. | |||
| 2018-06-07 | add test for #7595 | Ralf Jung | |
| 2018-06-07 | Merge PR #7735: Remove cross-crypto from Travis. It is still tested in ↵ | Emilio Jesus Gallego Arias | |
| GitLab CI. | |||
| 2018-06-07 | Remove cross-crypto from Travis. It is still tested in GitLab CI. | Théo Zimmermann | |
| This fixes #7734. | |||
| 2018-06-07 | Fix the checker by merely adapting the data structure. | Pierre-Marie Pédrot | |
| Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though. | |||
| 2018-06-07 | Fix #7615: Functor inlining drops universe substitution. | Pierre-Marie Pédrot | |
| We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case. | |||
| 2018-06-07 | Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided | Matthieu Sozeau | |
| 2018-06-07 | Merge PR #7706: Fix wrong deprecation msg | Pierre-Marie Pédrot | |
| 2018-06-07 | Merge PR #6874: [econstr] Some minor tweaks | Pierre-Marie Pédrot | |
| 2018-06-06 | Merge PR #7721: Add a note about [ci skip] in CI README. | Emilio Jesus Gallego Arias | |
| 2018-06-06 | [ci] [docker] Pin specific versions of OPAM CI dependencies. | Emilio Jesus Gallego Arias | |
| Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used. | |||
| 2018-06-06 | Add a note about [ci skip] in CI README. | Théo Zimmermann | |
| 2018-06-06 | Merge PR #7717: [ci] Temporal fix for CompCert | Gaëtan Gilbert | |
| 2018-06-06 | [ci] Temporal fix for CompCert | Emilio Jesus Gallego Arias | |
| https://github.com/AbsInt/CompCert/issues/234 | |||
| 2018-06-05 | Merge PR #7679: Clean native compilation of primitive projections | Maxime Dénès | |
| 2018-06-05 | Merge PR #7004: Make `simple apply` obey `Opaque` directive. | Pierre-Marie Pédrot | |
| 2018-06-05 | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | Maxime Dénès | |
| vm_compute and native_compute (partial fix to #7068; also fixes #7076)) | |||
| 2018-06-05 | Merge PR #7663: test suite: make target to regenerate failing output tests | Enrico Tassi | |
| 2018-06-05 | Improve links to SSR tactics, and some other improvements. | Théo Zimmermann | |
| 2018-06-05 | Merge PR #7464: Make whitespace linter not check for trailing space. | Maxime Dénès | |
| 2018-06-05 | Define rec_declaration in terms of prec_declaration. | SimonBoulier | |
| And similarly for fixpoint and cofixpoint. | |||
| 2018-06-05 | Update evarutil.mli | Matthieu Sozeau | |
| Actually all the new_ functions are in evarutil still | |||
| 2018-06-05 | Fix wrong deprecation msg | Matthieu Sozeau | |
| 2018-06-05 | Workaround a weird error of .. coqtop:: | Théo Zimmermann | |
| 2018-06-05 | Remove many abusive .. coqtop in SSR chapter. | Théo Zimmermann | |
| Many still remain. | |||
| 2018-06-05 | A few additional small fixes. | Théo Zimmermann | |
| 2018-06-05 | [sphinx] Fix missing indices warnings. | Théo Zimmermann | |
| 2018-06-05 | [ssr] index entry for "without loss", "suffices" and "generally have" | Enrico Tassi | |
| 2018-06-05 | [ssr] some fixes to the documentation markup | Enrico Tassi | |
| 2018-06-05 | [sphinx] Start fixing SSR chapter. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |