aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [api] Re-enable deprecation warnings.Gravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | With a bit of care we can enable full deprecation warnings again in this funny file.
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* Merge PR #6173: [printing] Deprecate all printing functions accessing the ↵Gravatar Maxime Dénès2017-11-21
|\ | | | | | | global proof.
| * [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ | | | | | | | | | | We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
* \ Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\ \
* \ \ Merge PR #6178: Have the coq_makefile timing test-suite print moreGravatar Maxime Dénès2017-11-21
|\ \ \
* \ \ \ Merge PR #6168: Add Equations to CIGravatar Maxime Dénès2017-11-21
|\ \ \ \
* \ \ \ \ Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \ \ \
| * | | | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | | | | | | | | | Was broken since 8.6.
* | | | | | Merge PR #6188: Rename coq-inferior.el -> inferior-coq.el to match provided ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | feature.
* \ \ \ \ \ \ Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6163: [dev] Remove deprecation warning from `base_include`Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | in make.
| | | | | | | | * | | | Add Equations to CIGravatar Matthieu Sozeau2017-11-20
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (clause "where" with implicit arguments)
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | unbound rel
| | | | | | | | * | | | | Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #4988.
| | | | | | | | | | | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
| | | | | | * | | | | [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
| | | | | | | * | | | [lib] Minor pending cleanup to consolidate helper function.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | While we are at it we refactor a few special cases of the helper.
| | | | | | * | | | [vernac] Increase table size.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As of Nov 2017, the standard number of entries is 85, it easily goes up with some other plugins, so 211 seems like a good compromise.
| | | | | | | | * [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | * Have the coq_makefile timing test-suite print moreGravatar Jason Gross2017-11-17
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
* | | | | | | Merge PR #6160: Fix gitlab for 4.06Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | local definitions)
* \ \ \ \ \ \ \ \ \ Merge PR #6104: Fixing encoding in coqdoc output tests.Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Fix micromega.ml to match generated file and enforce match in make.Gravatar Gaëtan Gilbert2017-11-16
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Mismatch probably caused by c5aca4005.
| | | | | | | | | * | Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6165.
| | | | | | | | * | [dev] Remove deprecation warning from `base_include`Gravatar Emilio Jesus Gallego Arias2017-11-15
| |_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | | Fix gitlab for 4.06Gravatar Gaëtan Gilbert2017-11-15
| |_|_|_|/ / / / |/| | | | | | |
| | | | | * | | Fix #5761: cbv on undefined evars under binders produces unbound relGravatar Gaëtan Gilbert2017-11-15
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * Fixing printing of tactics encapsulated as tacarg with Tacexp.Gravatar Hugo Herbelin2017-11-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * Using "l" printer for glob_constr, like for constr.Gravatar Hugo Herbelin2017-11-15
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f".
* | | | | | Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06Gravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6146: coq_makefile: document COQ_SRC_SUBDIRSGravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6138: Clean up/less files at rootGravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Gravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6058: Remove redundant env argument to Reduction.ccnvGravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6045: [travis] [coq] Complete 4.06.0 support.Gravatar Maxime Dénès2017-11-15
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | | | | | | | * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | * | | Fixing encoding in coqdoc output tests.Gravatar Hugo Herbelin2017-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | | | | | Move contributing files to .github/ sub-directory.Gravatar Théo Zimmermann2017-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The overall goal is to reduce the number of files at the root of the repository.
| | | | * | | | | | | Remove useless file README.doc.Gravatar Théo Zimmermann2017-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 13:08:56 +0000