interp · coq · Tangled

forked from coq/coq

coq interp

37 files

Hugo Herbelin · Move and export contract_curly_brackets in an ops file so that Rocq-lsp can use it. · 3w ago

abbreviation.ml

Abstract away the Summary reference type.

abbreviation.mli

Extend and cleanup the abbreviation API.

constrexpr_ops.ml

Move and export contract_curly_brackets in an ops file so that Rocq-lsp can use it.

constrexpr_ops.mli

Move and export contract_curly_brackets in an ops file so that Rocq-lsp can use it.

More explicit parameter names

constrextern.ml

Turn notation into a record

constrextern.mli

Pass printing flags functionally in constr printers

constrintern.ml

Move and export contract_curly_brackets in an ops file so that Rocq-lsp can use it.

constrintern.mli

Take into account that the type in PatCast is not a pattern.

Abstract away the Summary reference type.

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

Turn notation into a record

Make the Dumpglob API more algebraic.

Remove compat coq-core libraries (not executables)

Take into account that the type in PatCast is not a pattern.

Take into account that the type in PatCast is not a pattern.

Abstract away the Summary reference type.

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

implicit_quantifiers.ml

A richer type system for notation variables.

implicit_quantifiers.mli

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

Introduce PolyFlags to gather flags for polymorphic defs

Revert name change of univ_decl to sort_poly_decl

notation_ops.ml

More uniform naming in notation_ops.ml.

notation_ops.mli

A few comments about the API of notations.

notation_term.mli

A few comments about the API of notations.

Turn notation into a record

A few comments about the API of notations.

notationextern.ml

Turn notation into a record

notationextern.mli

[notation] Refactor internal representation of scopes stack

Fully separate ltac2 notation parsing from intern-time data

Fully separate ltac2 notation parsing from intern-time data

primNotations.ml

Use the VM for primitive token normalization.

primNotations.mli

Pass printing flags functionally in constr printers

A richer type system for notation variables.

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

Extend and cleanup the abbreviation API.

smartlocate.mli

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