| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | |
| I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. | |||
| 2017-11-17 | Have the coq_makefile timing test-suite print more | Jason Gross | |
| This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again. | |||
| 2017-11-16 | Merge PR #6160: Fix gitlab for 4.06 | Maxime Dénès | |
| 2017-11-16 | Merge PR #6148: [api] Another large deprecation, `Nameops` and friends. | Maxime Dénès | |
| 2017-11-16 | Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵ | Maxime Dénès | |
| local definitions) | |||
| 2017-11-16 | Merge PR #6104: Fixing encoding in coqdoc output tests. | Maxime Dénès | |
| 2017-11-16 | Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2 | Maxime Dénès | |
| 2017-11-16 | Fix micromega.ml to match generated file and enforce match in make. | Gaëtan Gilbert | |
| Mismatch probably caused by c5aca4005. | |||
| 2017-11-15 | Fix regression in treating Defined as defined | Tej Chajed | |
| Fixes #6165. | |||
| 2017-11-15 | Make list functions returning sumbools transparent | Tej Chajed | |
| Specifically Exists_dec, Forall_dec, and Forall_Exists_dec. | |||
| 2017-11-15 | [dev] Remove deprecation warning from `base_include` | Emilio Jesus Gallego Arias | |
| The warning created problems as OCaml restored the color printing tags when printing it, so users doing `Drop` and then `go ()` got color printing back after the warning. We should guard the console on `Drop` better, but this requires some (much needed) refactoring work in the toplevel. | |||
| 2017-11-15 | Fix gitlab for 4.06 | Gaëtan Gilbert | |
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | |||
| 2017-11-15 | Fixing printing of tactics encapsulated as tacarg with Tacexp. | Hugo Herbelin | |
| We preserve the level instead of resetting it at level 0. Probably it would be the same as giving level ltop since Tacexp apparently comes only from using a tactic in an Ltac "let", which is where I observed a problem. | |||
| 2017-11-15 | Using "l" printer for glob_constr, like for constr. | Hugo Herbelin | |
| This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f". | |||
| 2017-11-15 | Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06 | Maxime Dénès | |
| 2017-11-15 | Merge PR #6146: coq_makefile: document COQ_SRC_SUBDIRS | Maxime Dénès | |
| 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.] | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |