aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9554: Don't save expected failure logs from opened/ bugs.Maxime Dénès
Reviewed-by: maximedenes
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe ↵Maxime Dénès
binders. Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-02-13Mention Discourse in contributing guide.Théo Zimmermann
2019-02-13Suggest asking on Discourse or Gitter.Théo Zimmermann
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
2019-02-13Advertise code of conduct in contributing guide.Théo Zimmermann
2019-02-13Mention coq-community in the contributing guide.Théo Zimmermann
2019-02-13Document how to add people to the contributors team.Théo Zimmermann
2019-02-13Refresh contributing guide.Théo Zimmermann
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13more testsEnrico Tassi
2019-02-13refactor grammarEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
(when defining a new constant)
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
Ack-by: Zimmi48
2019-02-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-13Merge pull request coq/ltac2#92 from ejgallego/proofview+proof_infoPierre-Marie Pédrot
[coq] Adapt to coq/coq#9173
2019-02-13Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: mattam82 Ack-by: maximedenes Reviewed-by: ppedrot
2019-02-12Merge PR #9548: Almost fully type-safe gramlib implementationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-12Merge PR #9563: Improve the documentation of auto.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coqide.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
Mostly in the pattern ~~~ .. coqtop:: in Theorem foo : bla. Theorem bar : blah. (* nested proof error *) ~~~
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
In particular, mention that auto does not use full-blown apply.
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary.
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
2019-02-12Fix doc for coqtop:: undoGaëtan Gilbert
2019-02-12Increase sphinx recursion limitGaëtan Gilbert
Not sure why but it seems required for future commits.
2019-02-11Merge PR #9551: Small typos in the documentation.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
Reviewed-by: CohenCyril Fixes a bug introduced by PR #9341
2019-02-11[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
This is the completion of #9070, needed in order to serialize ssreflect programs properly. TTBOK this completes the interface for all generic arguments.
2019-02-11Merge PR #9544: [coqargs] Minor refactoring of error functions.Enrico Tassi
Reviewed-by: gares
2019-02-11Don't save expected failure logs from opened/ bugs.Gaëtan Gilbert
Grepping for "Error!" is how we decide if we exit with failure or not. I don't remember why I used the "==> FAILURE <==" string in the save-logs script but it was an error.
2019-02-11Merge PR #9531: [test-suite] Improve test for async workers.Enrico Tassi
Reviewed-by: gares
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-11[ide] fix unconditional goto-point on editing an error (fix #9488)Enrico Tassi
2019-02-11Almost fully type-safe implementation of camlp5.Pierre-Marie Pédrot
There are still minute uses of type-unsafe primitives. Most of them can be removed if I had a little higher dan in GADTs (or weeks to spare thinking about how non-interactive proofs can be performed) but one, which is really a potential source of unsoundness. The latter is not problematic as all uses in Coq are protected about the unsoundness proof, but the API is clearly deficient and needs to be fixed at some point.
2019-02-11Further propagation of well-typedness in Grammar.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 22:16:47 +0000