| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-10 | Merge PR #8104: Warnings on coercions used without being Imported | Enrico Tassi | |
| 2018-09-10 | Bump version number to 8.10+alpha. | Guillaume Melquiond | |
| 2018-09-10 | [dune] Add apidoc target using `odoc` | Emilio Jesus Gallego Arias | |
| We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems. | |||
| 2018-09-10 | [ci] [docker] Add more dependencies for Dune-aware jobs. | Emilio Jesus Gallego Arias | |
| - odoc: used to generate the ML API documentation by Dune's `@doc` target. - dune-release: Automatic OPAM package generation and release. Both packages require OCaml >= 4.02 thus installing on edge switches only. | |||
| 2018-09-10 | Ltac2 overlay. | Hugo Herbelin | |
| 2018-09-10 | Relying on the precomputation of the renaming also for new_evar_type. | Hugo Herbelin | |
| 2018-09-10 | Fixing ltac names interpretation in internals of pattern-matching compilation. | Hugo Herbelin | |
| The parts of pattern-matching compilation which generated names may generate names which collided with names of the Ltac environment. We fix it by avoiding the names of the Ltac environment. | |||
| 2018-09-10 | Fixing an inconsistency in interpreting Ltac names linking to binder names. | Hugo Herbelin | |
| The recursion names in fix and cofix were not renamed like other binders were. | |||
| 2018-09-10 | Moving part of pretyping dealing with ltac and renaming in new module GlobEnv. | Hugo Herbelin | |
| This module contains: - the former ExtraEnv in pretyping - a few functions to traverse binders in pretyping.ml and cases.ml - the part of pretyping dealing with genarg interpretation The dependency of pretyping in an interpretation of names as names of variables of identifier is now hidden in GlobEnv (no more explicit "lvar" management in pretyping.ml). Similarly for the interpretation of names as terms and for the interpretation of tactics-in-terms. We keep empty_lvar in Glob_ops for compatibility, even though it is a bit isolated there. | |||
| 2018-09-10 | Temptative clarification of the role of ltac_genargs field in ltac_var_map. | Hugo Herbelin | |
| 2018-09-10 | Minor cosmetic unifying of layout in pretyping.ml. | Hugo Herbelin | |
| 2018-09-10 | Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments. | Hugo Herbelin | |
| 2018-09-10 | Deprecate romega in favor of lia. | Vincent Laporte | |
| 2018-09-07 | Bvector: add BVeq and some notations | Yishuai Li | |
| 2018-09-07 | NArith: deprecate N2Bv_gen | Yishuai Li | |
| Use N2Bv_sized instead. | |||
| 2018-09-07 | Merge PR #8437: Recover lost snippet | Théo Zimmermann | |
| 2018-09-07 | Merge PR #8435: [dune] Fix build of coq_dune in 4.02.3 | Théo Zimmermann | |
| 2018-09-07 | Recover lost snippet | Matěj G | |
| This snippet on pattern matching got lost in the process of migrating to Sphynx. | |||
| 2018-09-07 | Merge PR #8428: Add utop to default.nix for use in nix-shell (see #8426). | Vincent Laporte | |
| 2018-09-07 | [dune] Fix build of coq_dune in 4.02.3 | Emilio Jesus Gallego Arias | |
| Fixes #8431 | |||
| 2018-09-07 | Fix bug #8432 : program fixpoint and universes | Matthieu Sozeau | |
| One didn't normalize the bodies of fixpoints according to the universe context, resulting in a type errors. Use EConstr.to_constr to ensure universes are normalized instead of using EConstr.Unsafe.to_constr. | |||
| 2018-09-07 | Warnings on coercions used without being Imported | Maxime Dénès | |
| This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes. | |||
| 2018-09-07 | Merge PR #8423: coqpp: allow DEPRECATED when declaring tactics | Pierre-Marie Pédrot | |
| 2018-09-07 | Canonical representation of kernel substitutions. | Pierre-Marie Pédrot | |
| For some reason the code was implementing substitutions as pairs of maps, but the invariant ensured actually no observable difference between fetching a module ident from one or the other. The split seems to be mostly due to historical reasons. We make this invariant static by representing substitutions as a single map. | |||
| 2018-09-07 | Remove dead code in Mod_subst. | Pierre-Marie Pédrot | |
| 2018-09-07 | Move to a team of code owners for the Nix files. | Théo Zimmermann | |
| 2018-09-07 | Add utop to default.nix for use in nix-shell (see #8426). | Théo Zimmermann | |
| 2018-09-07 | Merge PR #8426: [dune] [doc] Document `dune utop $lib` | Théo Zimmermann | |
| 2018-09-07 | Merge PR #8411: Changes to default.nix to be able to use Dune. | Vincent Laporte | |
| 2018-09-06 | Merge PR #8412: [dune] [ci] Fix and test release profile + use 1.1 ↵ | Gaëtan Gilbert | |
| dune-workspace | |||
| 2018-09-06 | [dune] [doc] Document `dune utop $lib` | Emilio Jesus Gallego Arias | |
| 2018-09-06 | [dune] [ci] Fix and test release profile + use 1.1 dune-workspace | Emilio Jesus Gallego Arias | |
| Dune 1.1 allows us to define the `env` flags in the workspace file, which is a better place than the current situation. Along the way, We fix the build flags for release mode [missing `-rectypes` and add a `release` build profile CI job. | |||
| 2018-09-06 | Deprecation warning in legacy tacextend.mlp | Vincent Laporte | |
| 2018-09-06 | deprecation is CODE instead of IDENT | Vincent Laporte | |
| 2018-09-06 | Bound proof-search in default program obligation tactic. | Matthieu Sozeau | |
| This issue was first reported on equations where a definition seemingly took all memory until Coq crashed. https://github.com/mattam82/Coq-Equations/issues/69 | |||
| 2018-09-06 | Fixing #8270 (cbn was calling zeta even when not asked for). | Hugo Herbelin | |
| 2018-09-06 | coqpp: allow DEPRECATED when declaring tactics | Vincent Laporte | |
| 2018-09-06 | Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate. | Pierre-Marie Pédrot | |
| 2018-09-06 | Merge PR #8394: Print the entire string to the CoqIDE screen, e.g. for ↵ | Pierre-Marie Pédrot | |
| "Print Options" | |||
| 2018-09-06 | Merge PR #8415: [bin] Fix binary location procedure to work with symlinks. | Pierre-Marie Pédrot | |
| 2018-09-06 | Merge PR #8420: [pfedit] Fix master build due to merge conflict | Gaëtan Gilbert | |
| 2018-09-06 | [pfedit] Fix master build due to merge conflict | Emilio Jesus Gallego Arias | |
| 2018-09-06 | Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with Program | Matthieu Sozeau | |
| 2018-09-06 | Override Dune derivation to update it before nixpkgs. | Théo Zimmermann | |
| As suggested by Vincent. | |||
| 2018-09-06 | Changes to default.nix to be able to use Dune. | Théo Zimmermann | |
| 2018-09-06 | Merge PR #8295: Fix #8291: print universe names in universe context for Check. | Matthieu Sozeau | |
| 2018-09-05 | Fixing #8416 (Print Assumptions missing module information from compiled files). | Hugo Herbelin | |
| This fixes the fix 1522b989 to #7192. The remaining Not_found after 1522b989 should have rung a bell that something was still strange. | |||
| 2018-09-05 | [bin] Fix binary location procedure to work with symlinks. | Emilio Jesus Gallego Arias | |
| In #7860 `Sys.executable_name` was introduced to locate coq private binaries; however, this breaks use cases with symlinks, such as Dune. In order to fix this, we adopt a simpler strategy; we will always adapt the name originally provided by the user, and only add a directory if it was originally present. This should work (hopefully) in all cases. This fixes `coqide` not working on Dune builds. | |||
| 2018-09-05 | Use more efficient accu check for cofix unfolding in native compilation. | Pierre-Marie Pédrot | |
| 2018-09-05 | Merge PR #6857: [build] Preliminary support for building with `dune`. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |