aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-08Merge PR #7739: add test for #7595Gaëtan Gilbert
2018-06-08Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ↵Théo Zimmermann
info
2018-06-08dev/doc/univpoly.{txt => md}, split off primitive projection infoGaëtan Gilbert
2018-06-08Merge PR #7417: Micromega clean-upThéo Zimmermann
2018-06-08Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gaëtan Gilbert
2018-06-07Micromega clean-upMaxime 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-07add test for #7595Ralf Jung
2018-06-07Merge PR #7735: Remove cross-crypto from Travis. It is still tested in ↵Emilio Jesus Gallego Arias
GitLab CI.
2018-06-07Remove cross-crypto from Travis. It is still tested in GitLab CI.Théo Zimmermann
This fixes #7734.
2018-06-07Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is providedMatthieu Sozeau
2018-06-07Merge PR #7706: Fix wrong deprecation msgPierre-Marie Pédrot
2018-06-07Merge PR #6874: [econstr] Some minor tweaksPierre-Marie Pédrot
2018-06-06Merge 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-06Add a note about [ci skip] in CI README.Théo Zimmermann
2018-06-06Merge PR #7717: [ci] Temporal fix for CompCertGaëtan Gilbert
2018-06-06[ci] Temporal fix for CompCertEmilio Jesus Gallego Arias
https://github.com/AbsInt/CompCert/issues/234
2018-06-05Merge PR #7679: Clean native compilation of primitive projectionsMaxime Dénès
2018-06-05Merge PR #7004: Make `simple apply` obey `Opaque` directive.Pierre-Marie Pédrot
2018-06-05Merge 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-05Merge PR #7663: test suite: make target to regenerate failing output testsEnrico Tassi
2018-06-05Merge PR #7464: Make whitespace linter not check for trailing space.Maxime Dénès
2018-06-05Update evarutil.mliMatthieu Sozeau
Actually all the new_ functions are in evarutil still
2018-06-05Fix wrong deprecation msgMatthieu Sozeau
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-06-05Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Pierre-Marie Pédrot
2018-06-05Merge PR #7690: Fixing typos in file Berardi.vPierre-Marie Pédrot
2018-06-05Merge PR #7646: Fix #4714: Stack overflow with native computePierre-Marie Pédrot
2018-06-05Merge PR #7099: Stronger invariants in unification signature.Matthieu Sozeau
2018-06-05Merge PR #7453: Refuse to parse empty [Context] command.Matthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-05Make direct invocations of `simple apply` obey `Opaque` directive.Maxime Dénès
When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
2018-06-04Merge PR #7315: An attempt to clarify error message for Arguments needing ↵Maxime Dénès
"rename" flag
2018-06-04Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Hugo Herbelin
2018-06-04Preserving "canonical" form of return predicate in native_compute.Hugo Herbelin
Note that the normalization of the context of the return predicate was not done by the native compilation but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval native_compute in fun x => match x in A y z return y = z with end.
2018-06-04Preserving "canonical" form of return predicate in vm_compute.Hugo Herbelin
Note that the normalization of the context of the return predicate was not done by the vm but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval vm_compute in fun x => match x in A y z return y = z with end.
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Hugo Herbelin
2018-06-04Merge PR #7481: document 7025 (coq_makefile flag variables)Maxime Dénès
2018-06-04Merge PR #7596: [ci] [windows] Use newer OCaml version.Michael Soegtrop
2018-06-04Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Pierre-Marie Pédrot
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
Most of it seems straightforward.
2018-06-04[termops] Update type of function, anyways not used in the codebase.Emilio Jesus Gallego Arias
Note that `Assumptions` ships its own copy, but for `Constr.t`.
2018-06-04[vernac] Switch back `auto_ind_decl` to Constr.Emilio Jesus Gallego Arias
AFAICT this tactic is always used on ground terms.
2018-06-04Make whitespace linter not check for trailing newlines.Gaëtan Gilbert
git does not know how to fix this automatically when they appear by removing a chunk of text at the end of the file. eg ``` foo bar ``` to ``` foo ```
2018-06-04Merge PR #7601: Fix notation for code snippet in documentationMaxime Dénès
2018-06-04Merge PR #7418: Actually take advantage of the normalization status of ↵Maxime Dénès
kernel closures.
2018-06-04test suite: make target to regenerate failing output testsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:27:14 +0000