aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 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-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-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
2019-02-11Introduce a GADT of well-typed grammar entries in Grammar.Pierre-Marie Pédrot
Not fully used yet, we rely on erasure casts for now.
2019-02-11Centralizing the calls to the global mutable grammar in Grammar.Pierre-Marie Pédrot
2019-02-11Specialize the intermediate types of the Grammar functor.Pierre-Marie Pédrot
Now that we depend on a module argument, we do not have to quantify over the arguments anymore.
2019-02-11Make Grammar truly functorial.Pierre-Marie Pédrot
The old implementation was simply hiding the fact that the functor relied on a generic data type. If we want to implement the grammar engine in a truly type-safe way, we need to make the ancilliary datatypes depend on the type parameters.
2019-02-11Move most of Gramext into Grammar.Pierre-Marie Pédrot
This module was defining unsafe functions and datatypes only relevant to the grammar engine. We hide them under the API so as to be able to later clean it up.
2019-02-11Merge PR #9465: [Nix-CI] Add iris and lambda-rustMaxime Dénès
Reviewed-by: maximedenes
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
We remove a few ad-hoc `exit` from the code as error handling really ought to be centralized.
2019-02-11Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-11Merge PR #9543: [ocamldebug] Fix load order after gramlib refactoring.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-11Merge PR #9522: Update link to refman for master branch.Vincent Laporte
Reviewed-by: vbgl
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-11Use math mode more.Tanaka Akira
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf. And two "x:T" are quoted.
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
Use LEFT DOUBLE QUOTATION MARK (U+201C) and RIGHT DOUBLE QUOTATION MARK (U+201D) instead of QUOTATION MARK (U+0022). QUOTATION MARK is formatted as same form both for opening and closing quotation mark.
2019-02-11Remove a space before closing double-quote.Tanaka Akira
2019-02-11[ocamldebug] Fix load order after gramlib refactoring.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9478: Remove the comment fields of locations.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:19:38 +0000