pretyping · coq · Tangled

forked from coq/coq

coq pretyping

85 files

Rodolphe Lepigre · Fix 20632. · 2w ago

arguments_renaming.ml

Abstract away the Summary reference type.

arguments_renaming.mli

Canonicalize the GlobRef map API from Arguments_renaming.

Use variable status to decide if a variable is section variable

Program "match" compilation supports inductive types with "let" in indices.

Add missing substitution in cbv for case iv

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

Abstract away the Summary reference type.

New evar kind for RR variables

[coercions] Disactivate by default the "ambiguous-paths" warning

coercionops.mli

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

Generalize get_sigmatypes

combinators.mli

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

constr_matching.ml

Remove the name field from projections.

constr_matching.mli

More type enforced "instantiation" of constr patterns

Move Printing Record tables into PrintingFlags

Remove compat coq-core libraries (not executables)

Remove calls to CanOrd in Evaluable.

Remove calls to CanOrd in Evaluable.

Use the now correct set and maps Names APIs.

Abstract away the Summary reference type.

define_evar_as_sort generate a flexible univ instead of rigid

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

Use the now correct set and maps Names APIs.

Undo adhoc exclusion of RR evar unification

find_subterm.ml

Add support for parsing elimination constraints

find_subterm.mli

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

More precise typing in genarg register default value

Stop using genarg for constr syntax extension

Added APIs for coqlsp

Added APIs for coqlsp

Enforce that genarg interp functions are at the correct type

Enforce that genarg interp functions are at the correct type

Stop using genarg for constr syntax extension

Stop using genarg for constr syntax extension

Introduce "Univ@{s;l}" notation for sort polymorphism

Introduce "Univ@{s;l}" notation for sort polymorphism

QGlobal is not QVar

Remove the name field from projections.

Use variable status to decide if a variable is section variable

Keep track of variable status (secvar or not) in named contexts

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

inductiveops.ml

fix: catch QGraph.EliminationError in make_allowed_elimination_actions

inductiveops.mli

Store template inductive data abstracted w.r.t. template levels.

Abstract away the Summary reference type.

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

case styles MatchStyle and RegularStyle are the same

Add Scheme All Command

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.

ltac_pretype.mli

Enable warning 70 (missing mli), add mli files

fix readback lifting bug

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

Stop using genarg for constr syntax extension

Stop using genarg for constr syntax extension

Stop using genarg for constr syntax extension

pretype_errors.ml

clean up exceptions of recursion_scheme_error

pretype_errors.mli

clean up exceptions of recursion_scheme_error

Fix Template application with 3 arguments needlessly unifying qvars to Prop

Collapse sort variables to Prop if they are >= Prop but not <= Type

printingFlags.ml

Use the now correct set and maps Names APIs.

printingFlags.mli

Use the now correct set and maps Names APIs.

Fix blatant bug in Program's papp

Rename Coq -> Rocq in various comments and doc

reductionops.ml

Use the now correct set and maps Names APIs.

reductionops.mli

Merge PR #22077: Reduction effects use econstr

Remove the name field from projections.

Reduce the exposure of QualityOrSet.t type in the Retyping API.

Use the now correct set and maps Names APIs.

Move Printing Record tables into PrintingFlags

More informative error message for "not an inductive product"

More informative error message for "not an inductive product"

templateArity.ml

Kernel keep qvar information for template inductives

templateArity.mli

Kernel keep qvar information for template inductives

typeclasses_errors.ml

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

typeclasses_errors.mli

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

Abstract away the Summary reference type.

typeclasses.mli

Canonicalize the GlobRef map API from Typeclasses.

Merge PR #22087: Move check_hyps_inclusion out of the kernel

feat: Add elaboration of fresh qualities

unification: protect CS resolution against call on illtyped terms

unification.mli

`rewrite in` no subterm error mention hyp instead of saying "in goal"

Merge PR #22574: fix readback lifting bug

Allow normalizing constructor parameters in the VM.