lib · coq · Tangled

forked from coq/coq

coq lib

59 files

Gaëtan Gilbert · CoqProject_file use exn instead of exit, and catch in rocqide · 3w ago

acyclicGraph.ml

Correctly implement graph traversal in AcyclicGraph.merge_with_root.

acyclicGraph.mli

Remove the unused AcyclicGraph.choose primitive.

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

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

document tactics/tactics.mli

document tactics/tactics.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.

Remove APIs that have been deprecated before 9.0.

Remove APIs that have been deprecated before 9.0.

Experiment: command modifier and tactic for allocation limits

Experiment: command modifier and tactic for allocation limits

coqProject_file.ml

CoqProject_file use exn instead of exit, and catch in rocqide

coqProject_file.mli

Apply suggestions.

Turn Suggest Proof Using into a warning and add quickfix

Turn Suggest Proof Using into a warning and add quickfix

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

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

deprecation.mli

Inline binder_constr

Add new [Rocq_package] module to lib.

Ignore COQPATH if it is equal to ROCQPATH

configure: add relocatable mode

rocqdep print location for module not found warning

Rename Coq -> Rocq in various comments and doc

Cleanup beautify handling

Cleanup beautify handling

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

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

Add an implementation of Hopcroft algorithm.

Add an implementation of Hopcroft algorithm.

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

instr.noperf.ml

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

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

add location notation information

add location notation information

Profiler attempt to measure heap size

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

Use Obj.field instead of copying summary_disk in objfile

Move print-mod-uid to main rocq exe instead of rocq repl

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

Rename Coq -> Rocq in various comments and doc

Cleanup beautify handling

Add format combinator Pp.fmt

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

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

rocq_package.ml

Add new [Rocq_package] module to lib.

rocq_package.mli

Add new [Rocq_package] module to lib.

Handle most unused-field warnings

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.

Move Flags.output_directory to System

Move Flags.output_directory to System

Unify nametab APIs using functors

Unify nametab APIs using functors

Use empty variants for Util.Empty

Remove APIs that have been deprecated before 9.0.

xml_datatype.mli

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