index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
reductionops.mli
Age
Commit message (
Expand
)
Author
2020-11-21
Documenting module Reductionops.Stack.
Hugo Herbelin
2020-11-21
Deduce Stack.decomp from Stack.strip_n_app.
Hugo Herbelin
2020-08-11
Move reduce_mind_case from Reductionops to Tacred.
Pierre-Marie Pédrot
2020-07-18
Merge PR #12588: [exn] Remove some uses of print
Pierre-Marie Pédrot
2020-07-10
Merge PR #12638: Some changes of representation in Tacred
Enrico Tassi
2020-07-09
[error handling] Anomaly in Conversion is a "precatchable_exception"
Emilio Jesus Gallego Arias
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-05
Further cleanup of dead code in the Reductionops API.
Pierre-Marie Pédrot
2020-07-05
Inline the Reductionops.fix_recarg function.
Pierre-Marie Pédrot
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-06-04
Further cleanup.
Pierre-Marie Pédrot
2020-06-04
Move the cbn reduction to its own file, and simplify the RAKAM accordingly.
Pierre-Marie Pédrot
2020-05-10
Further cleanup: remove the local_reduction_function type.
Pierre-Marie Pédrot
2020-05-10
No more local reduction functions in Reductionops.
Pierre-Marie Pédrot
2020-03-28
Remove some cruft from Reductionops API.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-14
Use thunks to univ instead of lazy constr for template typing
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-10
Remove various circumvolutions from reduction behaviors
Maxime Dénès
2019-05-07
Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.
Pierre-Marie Pédrot
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-04
Primitive integers
Maxime Dénès
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Proper record type and accessors for transparent states.
Pierre-Marie Pédrot
2018-11-19
Move transparent_state to its own module.
Pierre-Marie Pédrot
2018-10-30
Avoid redefining reduction functions in fun_ind
Maxime Dénès
2018-09-26
[print] Restrict use of "debug" Termops printer.
Emilio Jesus Gallego Arias
2018-09-06
Fixing #8270 (cbn was calling zeta even when not asked for).
Hugo Herbelin
2018-07-25
Merge PR #7889: Cleanup reduction effects: they only work on constants.
Pierre-Marie Pédrot
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-07-12
Cleanup reduction effects: they only work on constants.
Gaëtan Gilbert
2018-06-04
Stronger invariants in unification signature.
Pierre-Marie Pédrot
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-08
[compat] Remove "Refolding Reduction" option.
Emilio Jesus Gallego Arias
2018-03-05
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-02
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2017-12-12
Further clean-up in Reductionops, removing unused lift arguments.
Maxime Dénès
2017-12-09
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-06
Getting rid of the Update constructor in Reductionops.
Pierre-Marie Pédrot
2017-12-06
Getting rid of the Shift constructor in Reductionops.
Pierre-Marie Pédrot
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Fix a bug in cumulativity
Amin Timany
2017-06-13
Merge PR#714: Print feature Proof-of-Concept (episode 2)
Maxime Dénès
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
[next]
