aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-06Merge PR #9487: Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Enrico Tassi
Ack-by: Zimmi48 Reviewed-by: gares
2019-02-06Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Théo Zimmermann
2019-02-05Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constrMatthieu Sozeau
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: mattam82
2019-02-05Merge PR #9472: Add advice and an example to the documentation of fold.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive ↵Pierre-Marie Pédrot
records Reviewed-by: ppedrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-05Merge PR #9396: Skip indirection through Evd for obligation ustate manipulationMatthieu Sozeau
Reviewed-by: mattam82
2019-02-05Merge PR #8421: [dune] Fix Dune build in Windows.Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-02-04Merge PR #9470: the default branch of Mtac2 changed to masterEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-04Merge PR #9468: Remove AppVeyor: superseded by Azure.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-02-04the default branch of Mtac2 changed to masterbeta
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
In order for Dune to work in Windows we need to tweak some script calls, they need a POSIX shell and the `(run ...)` / `(system ...)` actions use `cmd.exe` on Windows. Hopefully, we will rely less on `bash` when Dune can understand Coq libraries. This affects shell scripts in `kernel/**.sh` for example. It is interesting to see how faster the Coq Windows build is with Dune + Windows. There are some problems with PATHs that prevent the test suite from working, these will be fixed in a future PR.
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: mattam82 Reviewed-by: ppedrot
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-04Overlays.Maxime Dénès
2019-02-04Primitive integersMaxime 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-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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:18:57 +0000