aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-01-17Remove the CoqIDE "Revert all Buffers" command.Pierre-Marie Pédrot
2020-01-17Remove the Tactic menu from CoqIDE.Pierre-Marie Pédrot
2020-01-16Merge PR #11400: Use the GTK completion widget in CoqIDEEmilio Jesus Gallego Arias
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-16[mltop] Remove error handling hacks in favor of default methods.Emilio Jesus Gallego Arias
2020-01-16[mltop] Store digest of modules used to compile files.Emilio Jesus Gallego Arias
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
2020-01-15Merge PR #11374: Close #11133Pierre-Marie Pédrot
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
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
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
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...Hugo 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
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
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Merge PR #11081: Native compute: cleanup temporary files on program exitPierre-Marie Pédrot
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the typ...Pierre-Marie Pédrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
2020-01-10Merge PR #11387: [refman] missing space in "Controlling the locality of comma...Théo Zimmermann
2020-01-10Merge PR #11385: Add badges for Docker Hub and coqorg/coq:latest versionThéo Zimmermann
2020-01-10missing spaceOlivier Laurent
2020-01-10Merge PR #11384: Fix build after merge of #11164Pierre-Marie Pédrot
2020-01-09Merge PR #11371: [merge script] Never bypass outdated branch sanity check.Jason Gross
2020-01-09Add badges for Docker Hub and coqorg/coq:latest versionErik Martin-Dorel
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Merge PR #11375: Add note about default goal selector next to bullet docsThéo Zimmermann
2020-01-08Merge PR #11378: let CI test bedrock2's 'tested' branch instead of 'master'Théo Zimmermann
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 21:16:06 +0000