aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-26Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)Emilio Jesus Gallego Arias
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-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-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
2018-04-17[default.nix] Build doc with nix-build.Théo Zimmermann
2018-04-17[stm] push functional API furtherEnrico Tassi
2018-04-17Merge PR #7242: Update the CI branch for Equations.Gaëtan Gilbert
2018-04-17Assign circleci files to @SkySkimmer, @ejgallegoGaëtan Gilbert
2018-04-17Merge PR #7278: pre-commit : do not fail miserably if git config has ↵Gaëtan Gilbert
`apply.whitespace = fix`
2018-04-17[stm] expose restore/backup since ~doc is (still) dummyEnrico Tassi
2018-04-17pre-commit : do not fail miserably if git config has `apply.whitespace = fix`Pierre Letouzey
Having `--whitespace=` on all `git apply` in this script should make it insensitive to user setup in `~/.gitconfig`, at least `[apply] whitespace = fix`. Note that even this way, this script remains hugely fragile and non mature, and would better *not* be set by default for everybody.
2018-04-17Merge PR #7277: Mention sphinxcontrib-bibtex in INSTALL.docThéo Zimmermann
2018-04-17Mention sphinxcontrib-bibtex in INSTALL.docMaxime Dénès
2018-04-17Merge PR #7276: Add some 8.8.0 contributors in creditsMaxime Dénès
2018-04-17Add some 8.8.0 contributors in creditsMaxime Dénès
2018-04-16Merge PR #7272: Mention other deprecations and fixes in CHANGESMaxime Dénès
2018-04-16Merge PR #7270: Sphinx doc fix indicesMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:53:55 +0000