| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-04 | Merge PR #9470: the default branch of Mtac2 changed to master | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-02-04 | Merge PR #9468: Remove AppVeyor: superseded by Azure. | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-02-04 | the default branch of Mtac2 changed to master | beta | |
| 2019-02-04 | Remove AppVeyor: superseded by Azure. | Théo Zimmermann | |
| 2019-02-04 | Merge PR #6914: Primitive integers | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot | |||
| 2019-02-04 | Merge PR #9317: Restrict universes in records. | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: mattam82 Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9144: Fixes #4633: clearer message unknown existential | Pierre-Marie Pédrot | |
| Ack-by: herbelin Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9409: Move non-primitive-record warning to ↵ | Pierre-Marie Pédrot | |
| declare_mutual_inductive_with_eliminations Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9437: Comment universe operations in Classes.context | Pierre-Marie Pédrot | |
| Reviewed-by: mattam82 Reviewed-by: ppedrot | |||
| 2019-02-04 | Merge PR #9386: Pass some files to strict focusing mode. | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot | |||
| 2019-02-04 | Overlays. | Maxime Dénès | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |