library · coq · Tangled

forked from coq/coq

coq library

25 files

Gaëtan Gilbert · Fix message for deprecated abbreviation and related doc · 3w ago

Deprecate the Coq-based APIs in Rocqlib.

Deprecate the Coq-based APIs in Rocqlib.

Remove compat coq-core libraries (not executables)

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.

Qualified names for custom entries

Qualified names for custom entries

Abstract away the Summary reference type.

More precise API for sets stored in Goption tables.

Deprecate Names.Label

Remove deprecated APIs in Lib (moved to Global)

Order search results by name after priority

Order search results by name after priority

Deprecate Names.Label

also check phase in add_leaf

library_info.ml

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

library_info.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.

Fix message for deprecated abbreviation and related doc

QGlobal is not QVar

Abstract away the Summary reference type.

Deprecate the Coq-based APIs in Rocqlib.

Abstract away the Summary reference type.

Abstract away the Summary reference type.