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
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
2017-06-04
Added support for a side effect on constants in reduction functions.
Thomas Sibut-Pinote
2017-04-27
Fix 4.04 warnings
Gaetan Gilbert
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-03-31
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-02-14
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
Cc API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
Rewrite API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Inv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Termops API using EConstr.
Pierre-Marie Pédrot
2016-09-09
no-refold patch
Paul Steckler
2016-07-03
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-01
Make semantics of whd_zeta consistent with other whd_* functions.
Maxime Dénès
2016-07-01
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-02-15
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
merge
Matej Kosik
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-02
Remove duplicate declarations.
Guillaume Melquiond
2015-12-17
CLEANUP: in the Reductionops module
Matej Kosik
2015-10-15
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-08-02
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
Documenting in passing.
Hugo Herbelin
2015-03-04
Fix bug #3532, providing universe inconsistency information when a
Matthieu Sozeau
2015-02-27
Add support so that the type of a match in an inductive type with let-in
Hugo Herbelin
2015-01-12
Update headers.
Maxime Dénès
2014-10-08
fix make mlidoc
Pierre Boutillier
2014-10-02
Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.
Matthieu Sozeau
[prev]
[next]
