aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-20Merge PR #11411: Checker validation now performed over reified dataGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-20Merge PR #11428: [mltop] Deprecate -load-ml options in anticipation of #11409Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-19Merge PR #11406: [dune] [dbg] Add support for coqtop in dune-dbgGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-19Merge PR #11214: Add a script to pin CI developments.Gaëtan Gilbert
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-19Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors ↵Pierre-Marie Pédrot
cons and nil Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot
2020-01-19Merge PR #11348: Discharge inductive types without rechecking themPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2020-01-19Removing text saying XML is future of PG, adding explicitly vscoq as a userHugo Herbelin
2020-01-17Merge PR #11413: [doc] [ltac2] Build Ltac2 documentationThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-17Merge PR #11410: [ci] [gitlab] Add `interruptible: true` to jobs.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17[doc] [ltac2] Build Ltac2 documentation [make build system]Emilio Jesus Gallego Arias
Build and install the Ltac2 documentation.
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
This partially fixes #10139 ; we now build the Ltac2 documentation and deploy it. The fix here can be used for inspiration to do the make-based part.
2020-01-17[dune] [dbg] Add support for coqtop in dune-dbgEmilio Jesus Gallego Arias
We also workaround problem #11405 , however, this should be reverted once the problem is fixed in OCaml upstream.
2020-01-17[ci] [gitlab] Add `interruptible: true` to jobs.Emilio Jesus Gallego Arias
When a newer pipeline contains the same job, the job can be interrupted, see: https://docs.gitlab.com/ee/ci/yaml/README.html#interruptible This should help with job limits (c.f. #11320 ) The patch is a bit unsatisfactory due to the duplication needed; we could define a base job and use extends, but not sure it is worth it for now.
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
Reviewed-by: maximedenes
2020-01-16Merge PR #11400: Use the GTK completion widget in CoqIDEEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-16Adding an option to change the autocompletion delay.Pierre-Marie Pédrot
2020-01-16Better handling of asynchronous completion.Pierre-Marie Pédrot
2020-01-16Hacking a completion widget based on the default GtkSourceView one.Pierre-Marie Pédrot
2020-01-16Move the per-architecture check of marshalled Uint63s to Values.Pierre-Marie Pédrot
2020-01-16Checker validation acts on object representations rather than objects.Pierre-Marie Pédrot
2020-01-16Code factorization in checker validation.Pierre-Marie Pédrot
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-15Merge PR #11374: Close #11133Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
preparation for direct discharge
2020-01-15Merge PR #11401: [nix] Dune-2 and other improvementsThéo Zimmermann
2020-01-15[Nix] Fix setup hook when COQPATH is not boundVincent Laporte
2020-01-15[Nix] Update reference to nixpkgsVincent Laporte
This brings dune at version 2.1.2
2020-01-15[Nix/CI] Add verdi-raftVincent Laporte
2020-01-15[Nix/CI] Update fiat_cryptoVincent Laporte
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with ↵Hugo Herbelin
decorations Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-14Merge PR #11392: Document the Set Default Proof Mode command.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to ↵Kazuhiko Sakaguchi
OCaml's string type Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: herbelin Ack-by: maximedenes Reviewed-by: pi8027
2020-01-13Merge PR #11081: Native compute: cleanup temporary files on program exitPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the ↵Pierre-Marie Pédrot
type of h. Reviewed-by: ppedrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio ↵Pierre-Marie Pédrot
(and not just… Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
The type of h is reconstructed to look as much as the initial type of h as possible.
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:16:11 +0000