aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-27Fixing a Scheme Equality anomaly with constants bound to inductive.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
We raise a normal error instead of an anomaly.
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
We raise a normal error instead of an anomaly. This fixes also #2550, #8492. Note in passing: While the case of a type "Inductive I := list I -> I" is difficult, the case of a "Inductive I := list nat -> I" should be easily doable.
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
Instead of looking into the name-oriented structure we look into the actual section structures. Note: together with #8475 this lets us remove UnivNames.add_global_universe.
2018-09-27Overlays for Ltac2 and Equations.Hugo Herbelin
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-27Merge PR #8562: [build] Re-enable warning 59.Gaëtan Gilbert
2018-09-27Merge PR #8571: [stdlib] Fix warning due to missing Declare Scope in BvectorHugo Herbelin
2018-09-27[stdlib] Fix warning due to missing Declare Scope in BvectorEmilio Jesus Gallego Arias
This broke the build so it should be merged quickly.
2018-09-27[ssr] [camlp5] Remove warning from camlp5Emilio Jesus Gallego Arias
Current compilation of ssrparser.ml4 produces: ``` coqp5 plugins/ssr/ssrparser.ml Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex]. ``` the solution is easy.
2018-09-27[dune] [coqide] Turn CoqIDE into a library.Emilio Jesus Gallego Arias
As noted by @anton-trunov, this is more useful for development and debug.
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features.
2018-09-26[build] Re-enable warning 59.Emilio Jesus Gallego Arias
After #8043 was fixed we can come back to a stricter warning profile for flambda.
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API.
2018-09-26Merge PR #8561: Fix votour compilation after #8102.Emilio Jesus Gallego Arias
2018-09-26Adapt to removal of section paths from kernel namesMaxime Dénès
2018-09-26Fix votour compilation after #8102.Pierre-Marie Pédrot
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-26Merge PR #8497: Use "rm -rf" in "make clean" so .coq-native directories are ↵Maxime Dénès
removed
2018-09-26Inline the definition of CClosure.mk_clos_deep.Pierre-Marie Pédrot
An important part of this function was dead code, due to the fact it was only used for whd evaluation of specific shapes of constr.
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)Maxime Dénès
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-26Merge PR #7571: [kernel] Compile with almost all warnings enabled.Maxime Dénès
2018-09-26Make the warning for non-imported hints compatible with internal backtracking.Pierre-Marie Pédrot
This prevents outputing false positives when the hints are discarded during proof search. Note that this is not sychronized with Ltac backtrack though, so your tactic may end up not using the hint and warning about it because a run of some auto function succeeded.
2018-09-26Merge PR #7309: Made names of existential variables interpretable as Ltac ↵Pierre-Marie Pédrot
variables.
2018-09-26Making cases.ml use state-passing instead of the evdref idiom.Pierre-Marie Pédrot
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-26Fix for Coq PR#8554 (term builder for tactic "change" takes an environment).Hugo Herbelin
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
And update documentation.
2018-09-26Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting ↵Pierre-Marie Pédrot
evars by name
2018-09-26[api] Two more missing deprecations.Emilio Jesus Gallego Arias
We missed two more constructor / record deprecation.
2018-09-25Fix an algorithmic issue in the vernac guardedness checker.Pierre-Marie Pédrot
Calling the O(n) EConstr.to_constr function at every node is a very bad idea (tm).
2018-09-25Merge PR #8535: Fixing #8532: regression in Print Assumptions within a functor.Pierre-Marie Pédrot
2018-09-25Merge PR #8552: [ci] [docker] elpi version 1.1.0Emilio Jesus Gallego Arias
2018-09-25Merge PR #8549: Fix issues introduced by the PDF manual mergeThéo Zimmermann
2018-09-25overlay to test elpi 1.1Enrico Tassi
2018-09-25elpi 1.1.0Enrico Tassi
2018-09-25Merge PR #8235: NArith: deprecate N2Bv_genHugo Herbelin
2018-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-25Mini refreshing layout Datatypes.v.Hugo Herbelin
2018-09-25Adding f_equal_dep in Logic.v.Hugo Herbelin
2018-09-25Fixing #8532 (regression in Print Assumptions within a functor).Hugo Herbelin
The regression was introduced in 1522b989 (PR #7193) which itself was fixing bug #7192. (Note another regression of the same commit which is fixed in #8416.)
2018-09-25Fix Sphinx manual targets.Théo Zimmermann
New targets refman, refman-html and refman-pdf. sphinx keeps its previous meaning (compatibility alias for refman-html). install-doc-sphinx has been accidentally renamed.
2018-09-25Fix title of Introduction chapter in HTML version.Théo Zimmermann
And location of footnote.
2018-09-25[doc] Rename credits-wrapper to credits and credits to credits-contentsClément Pit-Claudel
This ensures that previous links to 'credits.html' still point to the right page.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 23:26:57 +0000