| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-15 | Merge PR #6138: Clean up/less files at root | Maxime Dénès | |
| 2017-11-15 | Merge PR #6122: Remove dependency of test-suite on git (fix #5725). | Maxime Dénès | |
| 2017-11-15 | Merge PR #6058: Remove redundant env argument to Reduction.ccnv | Maxime Dénès | |
| 2017-11-15 | Merge PR #6045: [travis] [coq] Complete 4.06.0 support. | Maxime Dénès | |
| 2017-11-15 | Fix test-suite. | Robbert Krebbers | |
| 2017-11-14 | Get rid of ' notation for Zpos in QArith. | Robbert Krebbers | |
| 2017-11-14 | Fixes #6129 (declaration of coercions made compatible with local definitions). | Hugo Herbelin | |
| 2017-11-14 | One more step in fixing #5762 ("where" clause). | Hugo Herbelin | |
| We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not. | |||
| 2017-11-13 | Fixing 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-13 | Move 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-13 | Remove 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-13 | Change OCAMLRUNPARAM warning to mention OCaml 4.06 | Paul 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-13 | coq_makefile: document COQ_SRC_SUBDIRS | Enrico Tassi | |
| 2017-11-13 | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6136: Update and simplify README. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6126: Fix ci-bignums.sh "missing ]" error. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵ | Maxime Dénès | |
| type is unknown | |||
| 2017-11-13 | Merge PR #6117: Fix printing anomaly in conv | Maxime Dénès | |
| 2017-11-13 | Merge PR #6103: Hack to restore printing of glob_constr in debugger. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6071: [ci] Add Ltac2 | Maxime Dénès | |
| 2017-11-13 | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6052: [general] Move Tactypes to `interp` + API reordering. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac. | Maxime Dénès | |
| 2017-11-11 | Single quotes break on Windows | Carl Patenaude Poulin | |
| As it is, running a `Makefile.coq` on Windows produces the following error: `cut: ': No such file or directory` Changing to double quotes fixes this. | |||
| 2017-11-10 | Update and simplify README. | Théo Zimmermann | |
| 2017-11-09 | ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106) | Enrico Tassi | |
| 2017-11-09 | Fix 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-09 | Introduce default.nix for Nix users. | Théo Zimmermann | |
| This file can be used to get in an environment ready to compile Coq (with `nix-shell`) or to compile and install Coq (with `nix-build`). | |||
| 2017-11-08 | Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120. | Hugo Herbelin | |
| PR #1120 was still buggy for the following reasons: variables in the lhs of the notation were linked in the glob file while they have nowhere to link to (the binder is the notation string) [I thought the change I commited in links.html.out was actually improving but it was an overlook, sorry.] | |||
| 2017-11-08 | Adding 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-08 | Remove 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-08 | Merge PR #6100: [api] Remove 8.7 ML-deprecated functions. | Maxime Dénès | |
| 2017-11-08 | Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | ↵ | Maxime Dénès | |
| tac2 ]" | |||
| 2017-11-08 | Merge PR #6087: [feedback] Helper to print feedback messages in the console. | Maxime Dénès | |
| 2017-11-08 | Merge PR #6086: [ci] Switch VST back to upstream. | Maxime Dénès | |
| 2017-11-08 | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès | |
| 2017-11-08 | Fixing missing separator in an error message. | Hugo Herbelin | |
| The message is the "Conversion test raised an anomaly" one. | |||
| 2017-11-08 | Fixing an (apparently misplaced) spc in anomaly reporting message. | Hugo Herbelin | |
| 2017-11-07 | Hack 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-06 | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter | |
| not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | |||
| 2017-11-06 | Generalize the use of repr in Tac2stdlib. | Pierre-Marie Pédrot | |
| 2017-11-06 | Remove packaging scripts while waiting for a fix to #5998. | Théo Zimmermann | |
| This is a temporary commit which should be reverted once the issue is fixed. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |