aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-04Merge PR #9437: Comment universe operations in Classes.contextPierre-Marie Pédrot
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
2019-02-04Overlays.Maxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-02-04Dockerfile: update menhir from 20180530 to 20181113Vincent Laporte
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
2019-02-04Merge PR #9461: Fix default goal selector error message.Pierre-Marie Pédrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-02-02Merge PR #9395: Global [open Univ] in UStatePierre-Marie Pédrot
2019-02-01Adapt to https://github.com/coq/coq/pull/9410Maxime Dénès
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
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-02-01Merge PR #9415: Simplify the GitHub issue templateMaxime Dénès
2019-02-01Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`Maxime Dénès
2019-02-01Correct W-Ind.Tanaka Akira
2019-02-01The lowest universe level is 1.Tanaka Akira
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
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
2019-01-31Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds.Gaëtan Gilbert
2019-01-31Use λ instead of \lb.Tanaka Akira
2019-01-31The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.Tanaka Akira
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
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
2019-01-31Use "∀" and "λ" instead of \forall and \lambda.Tanaka Akira
2019-01-31Use math more.Tanaka Akira
2019-01-31Make parenthesis correctly matched.Tanaka Akira
2019-01-31\Sort is not a term.Tanaka Akira
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
2019-01-31Fix syntax of two lambda-abstractions.Tanaka Akira
2019-01-31Change {\Sort} to \Sort.Tanaka Akira
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 03:13:19 +0000