clib · coq · Tangled

forked from coq/coq

coq clib

78 files

Gaëtan Gilbert · Catch correct exn in CUnix.mktemp_dir · 3mo ago

Constr and HConstr: stop hashconsing in place

Constr and HConstr: stop hashconsing in place

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Handle most unused-field warnings

Tolerate adding constants between generating a side effect certificate and checking it

Use APIs new since ocaml 4.09

Use APIs new since ocaml 4.09

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Hashconsing try to avoid recomputing hashes

Cleanup hashcons APIs and fix hashconsing of modpaths

Validate Proof: detect missing constraints, error if any issues found

Search: allow typos when searching by string

Search: allow typos when searching by string

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Catch correct exn in CUnix.mktemp_dir

Update the OCaml headers to reflect the fact Coq is now Rocq.

Displays the differences between successive proof steps in coqtop and CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG.

Displays the differences between successive proof steps in coqtop and CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG.

Remove compat coq-core libraries (not executables)

Fully separate ltac2 notation parsing from intern-time data

Fully separate ltac2 notation parsing from intern-time data

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Hashconsing try to avoid recomputing hashes

Hashconsing try to avoid recomputing hashes

Improve performance of Weak.add

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Use APIs new since ocaml 4.09

Update the OCaml headers to reflect the fact Coq is now Rocq.

clib/int.ml micro-optim: use '%compare' rather than 'caml_int_compare'

clib/int.ml micro-optim: use '%compare' rather than 'caml_int_compare'

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

memprof_coq.memprof.ml

Stop explicitly starting memprof limits

memprof_coq.mli

Stop explicitly starting memprof limits

memprof_coq.std.ml

Stop explicitly starting memprof limits

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

mutex_aux_4.x.ml

[lib] [mutex] Fix build for OCaml 5.x due to missing caml_mutex_unlock

mutex_aux_5.0.ml

[lib] [mutex] Fix build for OCaml 5.x due to missing caml_mutex_unlock

mutex_aux_5.x.ml

[lib] [mutex] Fix build for OCaml 5.x due to missing caml_mutex_unlock

[lib] [mutex] Fix build for OCaml 5.x due to missing caml_mutex_unlock

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Change the failing behaviour of Option.get to an assertion failure.

Change the failing behaviour of Option.get to an assertion failure.

Update the OCaml headers to reflect the fact Coq is now Rocq.

orderedType.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Warnings with quickfix: now possible to delay quickfix printing

Warnings with quickfix: now possible to delay quickfix printing

Update the OCaml headers to reflect the fact Coq is now Rocq.

Infrastructure for import categories

Add a set primitive to the Range module.

Add a set primitive to the Range module.

Update the OCaml headers to reflect the fact Coq is now Rocq.

segmenttree.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Optimize the algorithm for unicode validation.

Rename Coq -> Rocq in various comments and doc

unicodetable_gen.ml

Precompute unicode tables to reduce exe size

unicodetable_gen.mli

Precompute unicode tables to reduce exe size

unicodetable.mli

Enable warning 70 (missing mli), add mli files

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

writeOnceArray.ml

Extrude NoDupArray into its own clib file, rename it to WriteOnceArray

writeOnceArray.mli

Extrude NoDupArray into its own clib file, rename it to WriteOnceArray