GGaëtan GilbertUse Obj.field instead of copying summary_disk in objfile
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Correctly implement graph traversal in AcyclicGraph.merge_with_root. When finding a node known to reach the target level, we do not forget to check whether we came from a path strictly above Set. As argued by the LLM report, this is unlikely to lead to a proof of False, but this is still a fairly damn serious issue. Fixes #22438: contradictory universe constraints pass acyclicity check. | 6 天前 | |
Remove the unused AcyclicGraph.choose primitive. | 3 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
document tactics/tactics.mli | 1 年前 | |
document tactics/tactics.mli | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Remove APIs that have been deprecated before 9.0. There are still a few that are actually used in the code. I left them around, for the lack of a better alternative. | 9 个月前 | |
Remove APIs that have been deprecated before 9.0. There are still a few that are actually used in the code. I left them around, for the lack of a better alternative. | 9 个月前 | |
warning for AllocLimit when memprof-limits not installed | 5 个月前 | |
warning for AllocLimit when memprof-limits not installed | 5 个月前 | |
Experiment: command modifier and tactic for allocation limits using https://guillaume.munch.name/software/ocaml/memprof-limits | 5 个月前 | |
Experiment: command modifier and tactic for allocation limits using https://guillaume.munch.name/software/ocaml/memprof-limits | 5 个月前 | |
Merge PR #22259: -package delay resolving until -I have been processed Reviewed-by: ppedrot Reviewed-by: rlepigre-skylabs-ai Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 6 天前 | |
Apply suggestions. | 2 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update comment | 5 个月前 | |
Inline binder_constr cf #21670 Mostly backwards compatible | 5 个月前 | |
Add new [Rocq_package] module to lib. | 2 个月前 | |
Ignore COQPATH if it is equal to ROCQPATH instead of warning and concatenating the 2 values | 1 年前 | |
configure: add relocatable mode | 1 年前 | |
rocqdep print location for module not found warning Fix #10815 | 2 个月前 | |
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 年前 | |
Cleanup beautify handling - remove Flags.beautify and beautify_file - `-beautify` is now only supported for compile mode - beautify printing is done incrementally between parsing and executing commands instead of all at once at the end of the file. This prevents errors from notations disappearing etc (close #8640). - cleanup comment handling functions (extract_comments and Pp comment printing) - stop checking the flag in constrextern (anyway extern should not be used in beautify since cf049ec9e1) | 6 个月前 | |
Cleanup beautify handling - remove Flags.beautify and beautify_file - `-beautify` is now only supported for compile mode - beautify printing is done incrementally between parsing and executing commands instead of all at once at the end of the file. This prevents errors from notations disappearing etc (close #8640). - cleanup comment handling functions (extract_comments and Pp comment printing) - stop checking the flag in constrextern (anyway extern should not be used in beautify since cf049ec9e1) | 6 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Add an implementation of Hopcroft algorithm. | 6 个月前 | |
Add an implementation of Hopcroft algorithm. | 6 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
add location notation information | 2 个月前 | |
add location notation information | 2 个月前 | |
Profiler attempt to measure heap size | 4 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Use Obj.field instead of copying summary_disk in objfile | 2 天前 | |
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. | 2 天前 | |
Cleanup beautify handling - remove Flags.beautify and beautify_file - `-beautify` is now only supported for compile mode - beautify printing is done incrementally between parsing and executing commands instead of all at once at the end of the file. This prevents errors from notations disappearing etc (close #8640). - cleanup comment handling functions (extract_comments and Pp comment printing) - stop checking the flag in constrextern (anyway extern should not be used in beautify since cf049ec9e1) | 6 个月前 | |
Add format combinator Pp.fmt This makes it possible to write messages in more usual ocaml style, eg `fmt "foo %s:@ bar" x` instead of `str "foo " ++ str x ++ str ":" ++ spc() ++ str "bar"`. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
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 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Add new [Rocq_package] module to lib. | 2 个月前 | |
Add new [Rocq_package] module to lib. | 2 个月前 | |
Handle most unused-field warnings The warning is locally disabled when the record is meant to be the result of some marshalling. There are a couple cases where I disabled the warning even though the field could probably be deleted, in particular zify (too many cases to want to bother) and some stm stuff with threads (not 100% sure we can delete those fields). | 7 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Move Flags.output_directory to System | 9 个月前 | |
Move Flags.output_directory to System | 9 个月前 | |
Unify nametab APIs using functors future work deprecate legacy APIs (use ModTypes.locate instead of locate_modtype etc) | 1 年前 | |
Unify nametab APIs using functors future work deprecate legacy APIs (use ModTypes.locate instead of locate_modtype etc) | 1 年前 | |
Use empty variants for Util.Empty | 2 个月前 | |
Remove APIs that have been deprecated before 9.0. There are still a few that are actually used in the code. I left them around, for the lack of a better alternative. | 9 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 |