| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-04 | Primitive integers | Maxime Dénès | |
| This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2019-02-04 | Dockerfile: update menhir from 20180530 to 20181113 | Vincent Laporte | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |