aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-04Merge PR #9144: Fixes #4633: clearer message unknown existentialPierre-Marie Pédrot
Ack-by: herbelin Reviewed-by: ppedrot
2019-02-04Merge PR #9409: Move non-primitive-record warning to ↵Pierre-Marie Pédrot
declare_mutual_inductive_with_eliminations Reviewed-by: ppedrot
2019-02-04Merge PR #9437: Comment universe operations in Classes.contextPierre-Marie Pédrot
Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
Reviewed-by: maximedenes Ack-by: ppedrot
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
Reviewed-by: gares
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #9461: Fix default goal selector error message.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
Reviewed-by: fajb
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
Ack-by: mattam82 Reviewed-by: ppedrot
2019-02-02Merge PR #9395: Global [open Univ] in UStatePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-01Fix default goal selector error message.Gaëtan Gilbert
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
Ack-by: JasonGross Reviewed-by: fajb Reviewed-by: jfehrle
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
We make `coqc` a truly standalone binary, whereas `coqtop` is restricted to interactive use. Thus, `coqtop -compile` will emit a warning and call `coqc`. We have also refactored `Coqargs` into a common `Coqargs` module and a compilation-specific module `Coqcargs`. This solves problems related to `coqc` having its own argument parsing, and reduces the number of strange argument combinations a lot.
2019-02-01Merge PR #9415: Simplify the GitHub issue templateMaxime Dénès
Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: tchajed
2019-02-01Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
Fixes #9453
2019-01-31add testEnrico Tassi
2019-01-31[proof] optimize proof always works on incomplete proofsEnrico Tassi
2019-01-31Merge PR #9449: Fix small errors in cic.rst (2nd).Théo Zimmermann
Reviewed-by: Zimmi48
2019-01-31Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-01-31Use λ instead of \lb.Tanaka Akira
The former is more succinct and intuitive.
2019-01-31The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.Tanaka Akira
c can be non-function since c:U. So, c c' is not typeable.
2019-01-31[ci] [ocaml] Fix OCaml trunk builds.Emilio Jesus Gallego Arias
2019-01-31Use "U" instead of "u" for a type.Tanaka Akira
2019-01-31Fix an index. The number of constructors is "l".Tanaka Akira
2019-01-31Merge PR #9442: Update pinned nixpkgs.Vincent Laporte
Ack-by: Zimmi48 Reviewed-by: vbgl
2019-01-31Use \Match for match construct.Tanaka Akira
2019-01-31Insert a space before \kwend.Tanaka Akira
2019-01-31Use \length for the function name of length.Tanaka Akira
2019-01-31Adjust spaces.Tanaka Akira
This commit basically ajusts spaces as - ∀x:T,t to ∀x:T,~t - λx:T.t to λx:T.~t - E;c:T to E;~c:T x and T are more related than T and t. So, T and t should not positioned closely than x and T. Unfortunately, they are formatted that T and t are positioned closely without "~". (Similary, c and T are more related than E and c.)
2019-01-31Use "∀" and "λ" instead of \forall and \lambda.Tanaka Akira
The former is more succinct and consistent with most of other parts in cic.rst.
2019-01-31Use math more.Tanaka Akira
Add :math:`...` for mathematical expressions.
2019-01-31Make parenthesis correctly matched.Tanaka Akira
2019-01-31\Sort is not a term.Tanaka Akira
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to "∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because \Sort is not a term. "S" is choosen to be consistent with the description of Inductive Definitions.
2019-01-31Use semicolon for separator of local contexts.Tanaka Akira
2019-01-31Don't line break at hyphen of compound words.Tanaka Akira
2019-01-31Move out a period and comma from :math:.Tanaka Akira
2019-01-31Nest :math: and parenthesis properly.Tanaka Akira
Exchange a closing parenthesis and a :math: closing backquote.
2019-01-31Fix syntax of two lambda-abstractions.Tanaka Akira
In the note about η-reduction, two lambda-abstraction used "," instead of ".".
2019-01-31Change {\Sort} to \Sort.Tanaka Akira
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have font changing effect. So, {\Sort} is same as \Sort now and the former is changed to latter in cic.rst.
2019-01-31Use \Prop, \Set and \Type defined in refman-preamble.sty.Tanaka Akira
2019-01-31Make "1" and "2" in "f1" and "f2" suffixes.Tanaka Akira
2019-01-31Make "1" and "n" in "u1" and "un" suffixes.Tanaka Akira
2019-01-31Remove "End TreeExample." line.Tanaka Akira
This corresponds to "Module TreeExample." removed at 2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
Reviewed-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-01-30Update Cachix signing key.Théo Zimmermann
2019-01-30Updated pinned nixpkgs.Théo Zimmermann
Use default OCaml version (4.06.1).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:28:56 +0000