aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-28Merge PR #7376: Fix gitlab ubuntu versionEmilio Jesus Gallego Arias
2018-04-28Fix gitlab ubuntu versionGaëtan Gilbert
Newer versions don't have the latex packages we want. see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131
2018-04-28Merge PR #7357: [CI] elpi 1.0 has an official opam packageEmilio Jesus Gallego Arias
2018-04-28Merge PR #7367: circle CI: do not use cache from old config.yml versionsEmilio Jesus Gallego Arias
2018-04-28Merge PR #6892: Cleanup implementation of normalize_context_set a bitPierre-Marie Pédrot
2018-04-27[CI] elpi 1.0 has an official opam packageEnrico Tassi
2018-04-27circle CI: do not use cache from old config.yml versionsGaëtan Gilbert
It begs things to break when the cache is out of sync with the system packages.
2018-04-27Merge PR #7358: Fix #7356: missing lift when interpreting default instances ↵Enrico Tassi
of evars
2018-04-27Merge PR #7351: Always print explanation for univ inconsistency, rm ↵Emilio Jesus Gallego Arias
Flags.univ_print
2018-04-26Merge PR #7321: configure: make -annotate fatal, and color error and warningsEmilio Jesus Gallego Arias
2018-04-26Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)Emilio Jesus Gallego Arias
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
2018-04-26Merge PR #7331: Fix a typo in the reference manual: <; -> <:Maxime Dénès
2018-04-26Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bitMaxime Dénès
2018-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
This removes the Flags.univ_print in the kernel, making it possible to put the univ printing flag ownership back in Detyping. The lazyness is because getting an explanation may be costly and we may discard it without printing. See benches - with lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console - without lazy https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console Notably without lazy mathcomp odd_order is +1.26% with some lines showing significant changes, eg PFsection11 line 874 goes from 11.76s to 13.23s (+12%). (with lazy the same development has -1% overall and the same line goes from 11.76s to 11.23s (-4%) which may be within noise range)
2018-04-25updating CI for Mtac2Beta Ziliani
2018-04-25Merge PR #7290: Update debugging.mdHugo Herbelin
2018-04-25Merge PR #6866: Slight improvement of messages related to direct and ↵Pierre-Marie Pédrot
indirect uses of tactic `clear`.
2018-04-25Merge PR #7322: Test suite Makefile: print message for failing tests as they ↵Enrico Tassi
come, misc improvements
2018-04-24Merge PR #307: Adding a flag to support different naming modes for evar ↵Pierre-Marie Pédrot
hypotheses.
2018-04-24Merge PR #6512: [api] Relocate `intf` modules according to dependency-order.Pierre-Marie Pédrot
2018-04-24Improving error message for clear tactic (and indirect uses of it).Hugo Herbelin
- Be more precise when trying to clear an hypothesis which occurs implicitly in a global constant. - Warns if destruct/induction cannot clear an hypothesis occurring implicitly in a global. In the first case, the change in situation Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a. is: - before: "a is used in conclusion" - after: "a is used implicitly in b in conclusion" In the second case: Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a. produces a warning: "Cannot remove a, it is used implicitly in b".
2018-04-24Adding a flag to support different naming modes for evar hypotheses.Hugo Herbelin
Four modes currently supported to deal with clashes: 1. Failing in case of clash 2. Renaming the most recent one 3. Renaming the previous hypothesis of same name if not a section variable 4. Renaming the previous hypothesis of same name even if a section variable The current mode is 3. Keeping it active by default
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
2018-04-23Merge PR #7152: [api] Remove dependency of library on Vernacexpr.Pierre-Marie Pédrot
2018-04-23Merge PR #7108: Legacy refiner handle eta-expanded case analysisPierre-Marie Pédrot
2018-04-23Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"Pierre-Marie Pédrot
2018-04-23Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.Pierre-Marie Pédrot
2018-04-23Fix a typo in the reference manual: <; -> <:Kazuhiko Sakaguchi
2018-04-22test suite: clean more things (glob, MExtraction.out, distclean aux)Gaëtan Gilbert
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
2018-04-22test suite: print message for failing tests as they comeGaëtan Gilbert
ie you might see make TEST bugs/closed/1337.v TEST bugs/closed/3263.v TEST bugs/closed/7777.v FAILED bugs/closed/3263.v.log TEST bugs/opened/1.v ... report: 3263 failed (should be closed)
2018-04-22test suite Makefile: do not use %.stamp for subsystem targetsGaëtan Gilbert
2018-04-22configure: make -annotate fatal, and color error and warningsGaëtan Gilbert
Warnings are just too hard to see. Also there is no point keeping a noop option except to point people at the replacement, which does not require configure to succeed.
2018-04-21Merge PR #7320: [ci] Also make some display targets for fiat-cryptoEmilio Jesus Gallego Arias
2018-04-21Merge PR #7319: CI: add fcsl-pcmEmilio Jesus Gallego Arias
2018-04-20[ci] Also make some display targets for fiat-cryptoJason Gross
This will catch things like https://github.com/coq/coq/pull/7025#issuecomment-381424489
2018-04-20CI: add fcsl-pcmAnton Trunov
2018-04-20Merge PR #6908: Move VM global tables from C to MLMaxime Dénès
2018-04-19Merge PR #7282: [toplevel] allow toploop_init change Coq optionsEmilio Jesus Gallego Arias
2018-04-19Merge PR #7219: merge script support https + typos in docMaxime Dénès
2018-04-19Merge PR #7248: Assign circleci files to @SkySkimmerMaxime Dénès
2018-04-19Merge PR #7294: fix Iris ciEmilio Jesus Gallego Arias
2018-04-19[toplevel] let toploop_init change Coq optionsEnrico Tassi
Toplevels may want to modify for example the Stm flags, which after #1108 are handled in a functional way.
2018-04-19Merge PR #7287: [default.nix] Build doc with nix-build.Vincent Laporte
2018-04-18Merge PR #7281: [stm] push functional API furtherEmilio Jesus Gallego Arias
2018-04-18Merge PR #7280: [stm] expose restore/backup since ~doc is (still) dummyEmilio Jesus Gallego Arias
2018-04-18CI: extract iris git version without using opamRalf Jung
2018-04-18fix iris-lambda-rust CIRalf Jung
2018-04-17Merge PR #7275: gitlab: separate opam-boot jobs, use opam init and OPAMROOTEmilio Jesus Gallego Arias
2018-04-17Merge PR #7268: Travis: cleanup environment variables a bit.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 02:32:25 +0000