aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-29Document that GITURL variables shouldn't have a trailing .git anymore.Théo Zimmermann
This allows to append /archive at the end.
2018-06-29Merge PR #7918: Mini-update of version history with recent changes.Théo Zimmermann
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Maxime Dénès
constr in Constr
2018-06-29Merge PR #7890: Inline a function from Quote used in setoid_ring.Maxime Dénès
2018-06-29Merge PR #7745: Make type Environ.globals abstract + simplify ↵Maxime Dénès
Environ.retroknowledge
2018-06-29Merge PR #7950: Documentation for 8.8.1Maxime Dénès
2018-06-28Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Emilio Jesus Gallego Arias
2018-06-28CHANGES for 8.8.1.Théo Zimmermann
2018-06-28Self-credit for the work done.Théo Zimmermann
I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
2018-06-28Merge PR #7948: Syntax for naming an existential variableThéo Zimmermann
2018-06-28Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.Michael Soegtrop
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Merge PR #7946: Update maintainers for native/VM files in pretypingThéo Zimmermann
2018-06-28Update gallina-extensions.rstAmbroise
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
2018-06-28Merge PR #7937: Mention Consortium in READMEThéo Zimmermann
2018-06-28Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.Théo Zimmermann
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28[env.env_rel_context.env_rel_ctx] -> [rel_context env]Gaëtan Gilbert
It's a bit shorter and more direct.
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-28Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.Pierre-Marie Pédrot
2018-06-28Update maintainers for native/VM files in pretypingMaxime Dénès
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-28Merge PR #7934: Add mit-plv/bedrock2-ci to CIEmilio Jesus Gallego Arias
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Merge PR #7939: Turn the CoqProject_file module into a pure ML fileEmilio Jesus Gallego Arias
2018-06-27Mention Consortium in READMEMaxime Dénès
We are now actively looking for sponsors, let's make our communication more visible.
2018-06-27Adding overlay.Hugo Herbelin
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
2018-06-27Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ↵Emilio Jesus Gallego Arias
in notations).
2018-06-27Slightly less crazy parsing algorithm for CoqProject_file.Pierre-Marie Pédrot
We use a buffer instead of O(n) appending to a string, and we also make the parser tail-call.
2018-06-27Turn CoqProject_file into a normal OCaml file.Pierre-Marie Pédrot
2018-06-27Fix 'unbound variable' issue on Windows packaging jobs.Théo Zimmermann
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-27CoqIDE scrolls the proof buffer down to the first goal.Cyprien Mangin
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
Was revealing a critical bug in VM universe handling introduced in 8.5.
2018-06-27Merge PR #7888: Clarify the message "this hint will only be used by eauto"Pierre-Marie Pédrot
2018-06-26Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftHugo Herbelin
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time.
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Pierre-Marie Pédrot
constants
2018-06-26Merge PR #7775: Fix handling of universe context for expanded program ↵Maxime Dénès
obligations.
2018-06-26Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵Maxime Dénès
build
2018-06-26Merge PR #7756: Fix #7608: missing num package in INSTALL documentation.Maxime Dénès
2018-06-26Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Maxime Dénès
2018-06-26Merge PR #7919: Fix equality check on global names from native compute.Maxime Dénès
2018-06-26Add overlay for elpiGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-26Add overlay for Equations, ElpiGaëtan Gilbert
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
Apparently it was not useful. I don't remember what I was thinking when I added it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 04:32:49 +0000