aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
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
2019-02-11Merge PR #9534: Workaround for CI not having enough RAM for bedrock2: ↵Emilio Jesus Gallego Arias
`-async-proofs-tac-j 1` Reviewed-by: ejgallego
2019-02-10Merge PR #9535: [readme] Add link to information about release plans.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-02-10Change "I" to "I_p".Tanaka Akira
Since the type of "c" is "I_p ...", the constructor should return the value of it.
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
2019-02-10Merge PR #9536: [ci] Remove unused bintray file.Maxime Dénès
Reviewed-by: maximedenes
2019-02-09remove `allow_failure: true` for bedrock2Samuel Gruetter
2019-02-09remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed ↵Samuel Gruetter
passed https://gitlab.com/coq/coq/-/jobs/158737429
2019-02-09Update link to refman and stdlib doc for master branch.Théo Zimmermann
2019-02-09[ci] Remove unused bintray file.Emilio Jesus Gallego Arias
Not needed anymore after Travis was removed.
2019-02-09[readme] Add link to information about release plans.Emilio Jesus Gallego Arias
This is a proposal to use the wiki to gather current information about the release process.
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile, and we use VERBOSE=1 for better debuggability
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-02-08[test-suite] Improve test for async workers.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
Reviewed-by: gares
2019-02-08Merge PR #9492: [stm] Filter some more arguments that shouldn't be sent to ↵Enrico Tassi
workers. Reviewed-by: gares
2019-02-08Merge PR #9504: Add print_pure_econstr signatureGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in ↵Théo Zimmermann
Docker Hub Reviewed-by: Zimmi48
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
This fixes #9484 .
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes
2019-02-08Merge PR #9515: [Gitlab-CI] Automatic deployment of the standard library ↵Emilio Jesus Gallego Arias
documentation to GH-pages Reviewed-by: ejgallego
2019-02-08Use math mode more.Tanaka Akira
2019-02-08Fix index of arguments of constructor in fixpoint.Tanaka Akira
In fixpoint typing rule section, a type of constructor is described twice: - ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s) - ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k) Both seems invalid. The former require that the number of parameters and the number of (non-parameter) constructor argumets is same. The latter require that the number of (non-parameter) constructor argumets and the number of inductive type arguments (including paramters) is same. Also, "k" is already used for the number of inductive types in a inductive definition. So, I changed the number of (non-parameter) constructor argumets to "m". I choose "m" because "m" is used for the purpose in the description for iota-reduction of destructors. Also, I changed the inductive type parameters and arguments of latter consistent with the former.
2019-02-08Change parameters p_1...p_r to q_1...q_r.Tanaka Akira
In the description of destructors, "Type of branches" section and "Typing rule" section shares the definition of "r" (and "s" from previous commit). However actual parameters are p_1...p_r in the former section and q_1...q_r in the latter section. I guess it's because the latter section uses p_1...p_l in other purpose: index of constructor for a inductive type. So, I change the parameter p_1...p_r to q_1...q_r in the former section to consistent with the latter section.
2019-02-08Change the index "p" to "s" in "type of branches".Tanaka Akira
In the description of destuctors, "Type of branches" section uses "p" as the number of arguments. It is confusing because "p" is used as the number of parameters. After the section, "Typing rule." section uses "s" without definition as I q1...qr t1...ts. It seems that it is the number of arguments. So, I changed "p" to "s". "s" is also confusing with sorts, though.
2019-02-08Change c to c' forgotten at exchanging c and c'.Tanaka Akira
In Cic admissible rules section, c and c' are exchanged at https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 . But the exchange is not complete. This commit complete it.
2019-02-08Remove spaces just before period (non-math mode).Tanaka Akira
2019-02-08Remove spaces just before comma (non-math mode).Tanaka Akira
2019-02-08Remove "'" accidentaly added.Tanaka Akira
"'" in the extended (k_i added) form of Fix syntax should be removed. In the following sentence, A_i' is referenced as A_i. ``` Each :math:`A_i` should be a type (reducible to a term) starting with at least :math:`k_i` products :math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` ``` Also, A_i' is used in ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i' and A_i' must not equal to ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'. The old reference manual, coq-8.7.2-reference-manual.pdf, doesn't have "'". They are added by https://github.com/coq/coq/commit/47dca6c5da585212f69b6b83b25896ff990781e3 which ports Cic document from TeX to sphinx. So, the change seems just an accident.
2019-02-08[Gitlab-CI] Automatic deployment of the standard library documentation to ↵Vincent Laporte
GH-pages
2019-02-08Add item in release-process.md to ease upcoming releases of Coq in Docker HubErik Martin-Dorel
Related: coq/bignums#17 [ci skip]
2019-02-07Merge PR #9499: [Gitlab-CI] Never attempt to build cachixThéo Zimmermann
Reviewed-by: Zimmi48
2019-02-07Merge PR #9477: Makefiles: Fixes for byte compilationEnrico Tassi
Reviewed-by: gares
2019-02-07Remove some non tailrec List.map from CList implementationsGaëtan Gilbert
Fix #9482
2019-02-07Merge PR #9475: Automatic deployment of the user manual to GH-PagesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: vbgl
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 01:36:49 +0000