aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-21Experimenting with a fine-grained cache for undefined evars in evinfos.Pierre-Marie Pédrot
2017-11-21Fix #6204: `refine` is exponential in the number of fresh evars that it creates.Pierre-Marie Pédrot
It is actually polynomial with a big exponent, probably quartic. This was due to the Proofview.unifiable algorithm that kept recomputing the free evars of an evar info. We share the computation instead. This does not make the contrived example compile in a reasonable amount of time, but it does make smaller instances compile way quicker than before. Indeed, the example is essentially quadratic in size as all evars refer to the previously defined ones in their signature.
2017-11-21Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesMaxime Dénès
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
Was broken since 8.6.
2017-11-20Merge PR #6188: Rename coq-inferior.el -> inferior-coq.el to match provided ↵Maxime Dénès
feature.
2017-11-20Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.Maxime Dénès
2017-11-20Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Maxime Dénès
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-20Merge PR #6163: [dev] Remove deprecation warning from `base_include`Maxime Dénès
2017-11-20Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵Maxime Dénès
in make.
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Maxime Dénès
(clause "where" with implicit arguments)
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Maxime Dénès
unbound rel
2017-11-19Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gaëtan Gilbert
Fixes #4988.
2017-11-19[plugins] Prepare plugin API for functional handling of state.Emilio Jesus Gallego Arias
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.
2017-11-19[lib] Minor pending cleanup to consolidate helper function.Emilio Jesus Gallego Arias
While we are at it we refactor a few special cases of the helper.
2017-11-19[vernac] Increase table size.Emilio Jesus Gallego Arias
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.
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-16Fix micromega.ml to match generated file and enforce match in make.Gaëtan Gilbert
Mismatch probably caused by c5aca4005.
2017-11-15Fix regression in treating Defined as definedTej Chajed
Fixes #6165.
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-15Fix gitlab for 4.06Gaëtan Gilbert
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaë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-15Fixing 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-15Using "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-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-14One 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 21:47:38 +0000