aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-06Makefiles: Fixes for byte compilationGaëtan Gilbert
- default targets don't depend on ocamlopt when it's unavailable - coqc.byte is built by byte target and coqc by coqbinaries target - unit tests use best ocaml - poly-capture-global-univs tests ml compilation with ocamlc - don't try to install .cmx and native-compute .o files cf https://github.com/coq/coq/issues/9464
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 #9486: Makefile.install should not have a target fooGaëtan Gilbert
2019-02-06Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Théo Zimmermann
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
Before #9263 this type was returned by the STM's `parse_sentence`, but the type was lost on the generalization to entries.
2019-02-05[Nix-CI] Add lambda-rustVincent Laporte
2019-02-05[Nix-CI] Add IrisVincent Laporte
2019-02-05[Nix-CI] Fix UnicoqVincent Laporte
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-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
This was dead code, it was never raised ever.
2019-02-05Remove the comment fields of locations.Pierre-Marie Pédrot
They didn't seem to be used at all.
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-05Documenting the Ltac Backtrace flag.Pierre-Marie Pédrot
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
This is only used for debugging, if a user wants more feedback she can turn on the option. Conversely, it has a cost for any tactic script, so it is wiser to disable it by default.
2019-02-05Add an option not to register Ltac backtraces.Pierre-Marie Pédrot
Fixes #7769: Better control over ltac backtraces. Fixes #7385: Tactic allocates gigabytes of RAM.
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-05OverlaysMaxime Dénès
2019-02-05Make Program a regular attributeMaxime Dénès
We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases.
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-02-04Enrich implicits for instancesJasper Hugunin
For compatibility, also * Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs * Add overlay for HoTT setting Arguments on some instances.
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-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
Ack-by: JasonGross Reviewed-by: fajb Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 06:55:40 +0000