| coqide-server: Renamed to rocqide-server | 1 个月前 |
| Fix Corelib detection with dune 3.24. | 1 个月前 |
| Merge PR #22429: Properly print module typing errors in rocqchk. Reviewed-by: gares Co-authored-by: gares <gares@users.noreply.github.com> | 8 小时前 |
| Catch correct exn in CUnix.mktemp_dir | 1 个月前 |
| Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 |
| PIDENT with exact ident and PKEYWORD have type `unit p` This means `x = IDENT "bla"` binds x to `()` instead of `"bla"`. Since binding to an exact value is useless no such code appears in the code base. TODO same transformation for FIELD NUMBER etc | 20 天前 |
| Merge PR #22399: Make Nativecode.string_of_kn really injective for good. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 7 小时前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| Merge PR #22372: Abstract away the Summary reference type. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 18 天前 |
| Introduce a function to get LStream locations relatively to the head. All callers only care about the positions of elements yet to come, and the current implementation is fundamentally leaky in terms of memory consumption as we keep all locations from the past. Being able to only look at stuff yet to come adds a clear separation between locations that ought to have been garbage collected and stuff that is still in the stream. The last source of location lookbehind is LStream.interval_loc which is used internally by the parsing engine. | 1 个月前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| Merge PR #22106: GenConstr can intern directly to constr Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 12 天前 |
| Merge PR #22399: Make Nativecode.string_of_kn really injective for good. Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 7 小时前 |
| Merge PR #22359: Move print-mod-uid to main rocq exe instead of rocq repl Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 6 小时前 |
| Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 19 天前 |
| Substitute all URLs to renamed repository. | 1 年前 |
| Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s` This also makes it stop relying on level tolerance. Fix #22324 | 18 天前 |
| Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 |
| Merge PR #22349: Fix singleton extraction after implicit erasure Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 6 天前 |
| Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 19 天前 |
| Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 19 天前 |
| Restore "Proof Using Clear Unused" | 2 个月前 |
| stm: report a lost master connection without matching strerror text Matching the text of system error messages is unreliable: on Windows FormatMessage translates them according to the system UI language, so the guard would not fire on a non-English machine. Instead the worker now lets Sys_error through its own marshal wrappers, which are not used by the master, and treats End_of_file and Sys_error alike in the main loop as the master having gone away. | 20 天前 |
| Fix repeated Coqargs parsing with ~init Coqargs.parse_args returns ordered list fields, but a returned value reused as init was treated as a reverse-order accumulator. This could reorder existing options. Normalize init before entering the parser and normalize the result afterward. Package resolution now lives in Coqinit after 0c884e3, so move the rocq-runtime.lib dependency from coqargs to sysinit and restore the parser purity boundary. | 4 天前 |
| Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 19 天前 |
| Merge PR #22359: Move print-mod-uid to main rocq exe instead of rocq repl Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 6 小时前 |
| Merge PR #22270: Fix notations and scopes for (hexa)decimal values Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 19 天前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native. | 8 小时前 |
| coqtop peek in coqloop code not clexer Fix incorrect locations when end of line spaces aren't stripped | 2 年前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| changelog for 9.3+rc1 | 1 个月前 |
| ocp-indent: strict_with=auto | 4 年前 |
| Link to code of conduct on website instead of duplicating it. | 11 个月前 |
| doc: five typos fixed in CONTRIBUTING.md | 1 年前 |
| {new,setoid_}ring -> ring I believe this renaming makes it easier for new contributors to discover the code of `ring`. | 5 年前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| fix pour install windows git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7545 85f007b7-540e-0410-9357-904b9bb8a0f7 | 20 年前 |
| Remove dummy version info from generated META. | 1 个月前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| SMTCoq now depends on trakt | 1 个月前 |
| Fix github CI badges in README | 1 年前 |
| Use the release profile for configure in opam The build instructions in the opam files correctly use `-p` for the builds themselves, but the configure script uses the default profile. The configure script now recognises -release in its first argument as meaning that `--profile=release` should be added to the `dune exec` invocation, and the opam files are updated to include this flag. | 1 年前 |
| Require dune version 3.21. | 2 个月前 |
| Backport opam file changes from repo Following https://github.com/ocaml/opam-repository/pull/27613 | 1 年前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| Merge PR #22356: Fix make dunestrap for upcoming dune Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com> | 19 天前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| Attempt to fix the nix setup. | 2 个月前 |
| Update flake.nix Co-authored-by: Ali Caglayan <alizter@gmail.com> | 3 年前 |
| Rename Coq -> Rocq in various comments and doc Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> Co-authored-by: Guillaume Melquiond <guillaume.melquiond@inria.fr> | 1 年前 |
| Require dune version 3.21. | 2 个月前 |
| rename package coq-core -> rocq-runtime | 1 年前 |
| Require dune version 3.21. | 2 个月前 |
| Require dune version 3.21. | 2 个月前 |
| opam package use relocatable mode | 11 个月前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| Delete coq, rocq-prover packages, add rocq-test-suite package coq and rocq-prover depend on stdlib so they don't really fit in this repo. | 1 年前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| coqide-server: Renamed to rocqide-server | 1 个月前 |
| [default.nix] Update the reference to nixpkgs; make it the default | 7 年前 |
