coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/reduction.ml

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

April 2024

coqbot-app[bot]
Merge PR #18864: Call guard checking with evar handlers in higher layers
committed

March 2024

Gaëtan Gilbert
Add optional ?evars argument to functions in reduction.ml
committed
Gaëtan Gilbert
Remove deprecated functions in reduction.ml
committed

October 2023

coqbot-app[bot]
Merge PR #17947: An update to #15582: clarify remaining obscure points regarding decompose_{lambda,prod}{_n,}{_assum,_decls} functions
committed
Hugo Herbelin
Renaming functions hnf_decompose_* to whd_decompose_*.
committed
Hugo Herbelin
In hnf_decompose_*_{decls,assum}, apply a uniform heuristic to expose more binders.
committed
Hugo Herbelin
Reduction.hnf_decompose_lambda_n_assum: typo in name of anomaly.
committed
Hugo Herbelin
Rename Reduction.hnf_decompose_lambda_n_decls using "_assum".
committed

September 2023

coqbot-app[bot]
Merge PR #18023: Some cleanup around CClosure
committed
Rodolphe Lepigre
Move [RedFlags] out of [CClosure].
committed

May 2023

coqbot-app[bot]
Merge PR #17453: Kernel: split reduction.ml to have conversion-related functions in conversion.ml
committed

April 2023

Gaëtan Gilbert
Kernel: split reduction.ml to have conversion-related functions in conversion.ml
committed

February 2023

coqbot-app[bot]
Merge PR #17204: Remove unused kernel reduction API
committed
coqbot-app[bot]
Merge PR #16995: Fast path interleaved in conversion
committed
Pierre-Marie Pédrot
Remove whd_betaiota from kernel reduction.
committed
Pierre-Marie Pédrot
Remove whd_betaiotazeta from kernel reduction.
committed
Gaëtan Gilbert
Fast path interleaved in conversion
committed

January 2023

coqbot-app[bot]
Merge PR #17091: Introduce relevance variables in the conversion engine.
committed
Pierre-Marie Pédrot
Introduce relevance variables in the conversion engine.
committed
coqbot-app[bot]
Merge PR #15582: Addressing proposal #15562: cleaning API of functions for destructing/constructing abstractions or products wrt contexts
committed

December 2022

Hugo Herbelin
Tentatively renaming prod_applist_assum & cie into prod_applist_decls
committed
Hugo Herbelin
Applying proposal #15562: uniformly-named iterated lambda/prod destructors.
committed

November 2022

coqbot-app[bot]
Merge PR #16825: Do not nf-βι normalize case-related error messages in Type_errors.
committed
Pierre-Marie Pédrot
Do not nf-βι normalize case-related error messages in Type_errors.
committed
coqbot-app[bot]
Merge PR #16775: Preserve more sharing in CClosure strong reduction
committed
Pierre-Marie Pédrot
Expose strong normalization over constrs rather than fconstrs.
committed

September 2022

coqbot-app[bot]
Merge PR #16442: Introduce a dedicated type for evar instances.
committed
Pierre-Marie Pédrot
Introduce a dedicated type for evar instances.
committed
coqbot-app[bot]
Merge PR #16480: Generalize kernel evar handling
committed
Pierre-Marie Pédrot
Wrap the evar expander type into an explicit record.
committed

June 2022

coqbot-app[bot]
Merge PR #15807: Delay Universe Substitution in CClosure
committed
Gaëtan Gilbert
Delay Universe Substitution in CClosure
committed

April 2022

coqbot-app[bot]
Merge PR #15662: inferCumulativity: do not unfold constants unless necessary
committed
Gaëtan Gilbert
inferCumulativity: do not unfold constants unless necessary
committed
coqbot-app[bot]
Merge PR #15890: Remove universe inference from the kernel.
committed
Pierre-Marie Pédrot
Move inferred_universes from Reduction to Reductionops.
committed
Pierre-Marie Pédrot
Remove the universe-inferring conversion functions from the Reduction API.
committed

March 2022

coqbot-app[bot]
Merge PR #15856: Remove the univ_of_sort function from the API.
committed
Pierre-Marie Pédrot
Move UniverseInconsistency from Univ to UGraph.
committed
Pierre-Marie Pédrot
Invert the dependency between Sorts and UGraph.
committed
coqbot-app[bot]
Merge PR #15837: Reduce Universe.t footprint
committed
Pierre-Marie Pédrot
Reduce the use of Universe.t in the kernel in favour of Sorts.t.
committed

February 2022

coqbot-app[bot]
Merge PR #15453: Computation of the guardedness of a subterm assumes too strong invariants on the internal form of fixpoints
committed
coqbot-app[bot]
Merge PR #15575: Use a dummy term for SProp conversion
committed
Pierre-Marie Pédrot
Use a faster irrelevance check for constants and constructors in conversion.
committed
Pierre-Marie Pédrot
Introduce a new irrelevant term in the reduction machine.
committed