index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
romega
/
const_omega.mli
Age
Commit message (
Expand
)
Author
2018-09-25
Remove romega
Vincent Laporte
2018-03-06
romega: get rid of EConstr.Unsafe
Pierre Letouzey
2018-02-12
[engine] Remove ghost parameter from `Proofview.Goal.t`
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-05
romega: takes advantage of context variables with body
Pierre Letouzey
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-05-24
ROmega: division-aware ReflOmegaCore, allowing trace without terms
Pierre Letouzey
2017-05-22
ROmega : O_STATE turned into a O_SUM
Pierre Letouzey
2017-05-22
ROmega: less contructors in the final omega trace
Pierre Letouzey
2017-05-22
ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT
Pierre Letouzey
2017-05-22
romega: no more normalization trace, replaced by some Coq-side computation
Pierre Letouzey
2017-05-22
romega: use N instead of nat for Tvar
Pierre Letouzey
2017-05-22
romega: discard constructor D_mono (shorter trace + fix a bug)
Pierre Letouzey
2017-04-24
Removing trivial compatibility layer in refl_omega.
Pierre-Marie Pédrot
2014-12-09
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
