| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-04 | Merge PR #9368: Discard argument names of section variables on section close | Pierre-Marie Pédrot | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries. | Maxime Dénès | |
| Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-02-04 | Merge PR #9426: [test-suite] Fix display of check. | Enrico Tassi | |
| Reviewed-by: gares | |||
| 2019-02-04 | Merge PR #9454: Fix off-by-one error in nat syntax warnings | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9452: [proof] optimize proof always works on incomplete proofs | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9461: Fix default goal selector error message. | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9291: Do not take universes into account in lia reification. | Frédéric Besson | |
| Reviewed-by: fajb | |||
| 2019-02-02 | Merge PR #9250: coqchk: fix check for kelim with functors | Pierre-Marie Pédrot | |
| Ack-by: mattam82 Reviewed-by: ppedrot | |||
| 2019-02-02 | Merge PR #9395: Global [open Univ] in UState | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-02-01 | Fix default goal selector error message. | Gaëtan Gilbert | |
| 2019-02-01 | Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zify | Vincent 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-01 | Merge PR #9415: Simplify the GitHub issue template | Maxime Dénès | |
| Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: tchajed | |||
| 2019-02-01 | Merge 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-31 | Fix off-by-one error in nat syntax warnings | Jason Gross | |
| Fixes #9453 | |||
| 2019-01-31 | add test | Enrico Tassi | |
| 2019-01-31 | [proof] optimize proof always works on incomplete proofs | Enrico Tassi | |
| 2019-01-31 | Merge PR #9449: Fix small errors in cic.rst (2nd). | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-01-31 | Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-01-31 | Use λ instead of \lb. | Tanaka Akira | |
| The former is more succinct and intuitive. | |||
| 2019-01-31 | The 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-31 | Use "U" instead of "u" for a type. | Tanaka Akira | |
| 2019-01-31 | Fix an index. The number of constructors is "l". | Tanaka Akira | |
| 2019-01-31 | Merge PR #9442: Update pinned nixpkgs. | Vincent Laporte | |
| Ack-by: Zimmi48 Reviewed-by: vbgl | |||
| 2019-01-31 | Use \Match for match construct. | Tanaka Akira | |
| 2019-01-31 | Insert a space before \kwend. | Tanaka Akira | |
| 2019-01-31 | Use \length for the function name of length. | Tanaka Akira | |
| 2019-01-31 | Adjust 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-31 | Use "∀" 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-31 | Use math more. | Tanaka Akira | |
| Add :math:`...` for mathematical expressions. | |||
| 2019-01-31 | Make 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-31 | Use semicolon for separator of local contexts. | Tanaka Akira | |
| 2019-01-31 | Don't line break at hyphen of compound words. | Tanaka Akira | |
| 2019-01-31 | Move out a period and comma from :math:. | Tanaka Akira | |
| 2019-01-31 | Nest :math: and parenthesis properly. | Tanaka Akira | |
| Exchange a closing parenthesis and a :math: closing backquote. | |||
| 2019-01-31 | Fix syntax of two lambda-abstractions. | Tanaka Akira | |
| In the note about η-reduction, two lambda-abstraction used "," instead of ".". | |||
| 2019-01-31 | Change {\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-31 | Use \Prop, \Set and \Type defined in refman-preamble.sty. | Tanaka Akira | |
| 2019-01-31 | Make "1" and "2" in "f1" and "f2" suffixes. | Tanaka Akira | |
| 2019-01-31 | Make "1" and "n" in "u1" and "un" suffixes. | Tanaka Akira | |
| 2019-01-31 | Remove "End TreeExample." line. | Tanaka Akira | |
| This corresponds to "Module TreeExample." removed at 2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833. | |||
| 2019-01-31 | Merge PR #8720: [Numeral notations] Use Coqlib registered constants | Emilio Jesus Gallego Arias | |
| Reviewed-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl | |||
| 2019-01-30 | Update Cachix signing key. | Théo Zimmermann | |
| 2019-01-30 | Updated pinned nixpkgs. | Théo Zimmermann | |
| Use default OCaml version (4.06.1). | |||
| 2019-01-30 | Merge PR #9440: Create deployment environment for Cachix. | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-01-30 | Create deployment environment for Cachix. | Théo Zimmermann | |
| 2019-01-30 | [toplevel] Deprecate the `-compile` flag in favor of `coqc`. | Emilio Jesus Gallego Arias | |
| This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments. | |||
| 2019-01-29 | Merge PR #9417: Update update-compat.py script | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |