aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-16Merge PR #6160: Fix gitlab for 4.06Maxime Dénès
2017-11-16Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Maxime Dénès
2017-11-16Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Maxime Dénès
local definitions)
2017-11-16Merge PR #6104: Fixing encoding in coqdoc output tests.Maxime Dénès
2017-11-16Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2Maxime Dénès
2017-11-15Fix gitlab for 4.06Gaëtan Gilbert
2017-11-15Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06Maxime Dénès
2017-11-15Merge PR #6146: coq_makefile: document COQ_SRC_SUBDIRSMaxime Dénès
2017-11-15Merge PR #6138: Clean up/less files at rootMaxime Dénès
2017-11-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
2017-11-15Merge PR #6058: Remove redundant env argument to Reduction.ccnvMaxime Dénès
2017-11-15Merge PR #6045: [travis] [coq] Complete 4.06.0 support.Maxime Dénès
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-13Fixing encoding in coqdoc output tests.Hugo Herbelin
The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
2017-11-13Move contributing files to .github/ sub-directory.Théo Zimmermann
The overall goal is to reduce the number of files at the root of the repository.
2017-11-13Remove useless file README.doc.Théo Zimmermann
This file is useless because all the information it contains is also in INSTALL.doc. The overall goal is to reduce the number of files at the root of the repository.
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-13Change OCAMLRUNPARAM warning to mention OCaml 4.06Paul Steckler
2017-11-13[ci] [coq] Complete 4.06.0 support.Emilio Jesus Gallego Arias
Due to an API change in laglgtk, we need to update CoqIDE. We use a makefile hack so it can compile with lablgtk < 2.8.16, another option would be to require 2.8.16 as a minimal dependency. We also refactor travis to test more lablgtk versions. We also need to account for improved attribute handling in 4.06.0, in particular module aliases will propagate the deprecation status. Fixes #6140.
2017-11-13coq_makefile: document COQ_SRC_SUBDIRSEnrico Tassi
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6136: Update and simplify README.Maxime Dénès
2017-11-13Merge PR #6126: Fix ci-bignums.sh "missing ]" error.Maxime Dénès
2017-11-13Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵Maxime Dénès
type is unknown
2017-11-13Merge PR #6117: Fix printing anomaly in convMaxime Dénès
2017-11-13Merge PR #6103: Hack to restore printing of glob_constr in debugger.Maxime Dénès
2017-11-13Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998.Maxime Dénès
2017-11-13Merge PR #6071: [ci] Add Ltac2Maxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-13Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.Maxime Dénès
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-10Update and simplify README.Théo Zimmermann
2017-11-09Fix ci-bignums.sh "missing ]" error.Gaëtan Gilbert
It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
2017-11-08Adding a debugging printer for ident maps whose codomain type is unknown.Hugo Herbelin
Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer.
2017-11-08Remove dependency of test-suite on git (fix #5725).Théo Zimmermann
The two lines that this commit remove are spurious as a `git clean -dfx || true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`.
2017-11-08Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Maxime Dénès
2017-11-08Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | ↵Maxime Dénès
tac2 ]"
2017-11-08Merge PR #6087: [feedback] Helper to print feedback messages in the console.Maxime Dénès
2017-11-08Merge PR #6086: [ci] Switch VST back to upstream.Maxime Dénès
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-08Fixing missing separator in an error message.Hugo Herbelin
The message is the "Conversion test raised an anomaly" one.
2017-11-08Fixing an (apparently misplaced) spc in anomaly reporting message.Hugo Herbelin
2017-11-07Hack to restore printing of glob_constr in debugger.Hugo Herbelin
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
We do up to `Term` which is the main bulk of the changes.
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
This will allow to merge back `Names` with `API.Names`
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
not "first [ progress tac1 | progress tac2 ]". And add a missing backslash.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 03:01:12 +0000