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-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
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
[next]
