aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-21Experimenting with a fine-grained cache for undefined evars in evinfos.Pierre-Marie Pédrot
2017-11-21Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Maxime Dénès
2017-11-21Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Maxime Dénès
2017-11-21Merge PR #6178: Have the coq_makefile timing test-suite print moreMaxime Dénès
2017-11-21[stm] Allow delayed constant in interactive mode.Emilio Jesus Gallego Arias
This setting is a debug assertion, due to the many flags we still over-approximate setting the flag to true to all interactive environments. [So the assert is checked in vo compilation] Fixes #6152.
2017-11-21Merge PR #6168: Add Equations to CIMaxime Dénès
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-20Fixing factorization of recursive notations in the case of an atomic separator.Hugo Herbelin
This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
2017-11-20Remove pidentref grammar entry.Gaëtan Gilbert
Replaced by ident_decl in #688.
2017-11-20Disable whitespace linter for .out files.Gaëtan Gilbert
2017-11-20Check findlib version in configure (fix #4270).Gaëtan Gilbert
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-20Add Equations to CIMatthieu Sozeau
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-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-19Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gaëtan Gilbert
Fixes #4988.
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
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`.
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-19Remove branch on caml version >= 3.10 from configure.Gaëtan Gilbert
We require 4.02.3.
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-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-17Have the coq_makefile timing test-suite print moreJason Gross
This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 02:18:37 +0000