plugins/micromega · coq · Tangled

forked from coq/coq

coq plugins micromega

39 files

Pierre-Marie Pédrot · Abstract away the Summary reference type. · 2mo ago

.ocamlformat-ignore

ocamlformat: use whitelist instead of blacklist

Handle most unused-field warnings

certificate.mli

Rocqify some comments and description messages in plugins/.

coq_micromega.ml

Remove more global lazys

coq_micromega.mli

Rocqify some comments and description messages in plugins/.

Rocqify some comments and description messages in plugins/.

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

Remove compat coq-core libraries (not executables)

g_micromega.mlg

rename package coq-core -> rocq-runtime

g_micromega.mli

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

rename package coq-core -> rocq-runtime

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.

Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

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

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

ZMicromega depends on BinInt not ZArith_base; deprecate Ztac

ZMicromega depends on BinInt not ZArith_base; deprecate Ztac

Rocqify some comments and description messages in plugins/.

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.

persistent_cache.ml

Rocqify some comments and description messages in plugins/.

persistent_cache.mli

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

Rocqify some comments and description messages in plugins/.

Rocqify some comments and description messages in plugins/.

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

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

[micromega] Add numerical compatibility layer.

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.

[micromega] Use `minus_one` built-in zarith constant.

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.

Abstract away the Summary reference type.

wit_tactic top type is tacvalue