| Age | Commit message (Expand) | Author |
|---|
| 2018-09-25 | Remove romega | Vincent Laporte |
| 2018-09-24 | [engine] Remove and deprecate `nf_enter` et al. | Emilio Jesus Gallego Arias |
| 2018-09-11 | Merge PR #8425: Deprecate romega in favor of lia | Pierre-Marie Pédrot |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin |
| 2018-09-10 | Deprecate romega in favor of lia. | Vincent Laporte |
| 2018-09-05 | [build] Preliminary support for building Coq with `dune`. | Emilio Jesus Gallego Arias |
| 2018-07-02 | Moving various ml4 files to mlg. | Pierre-Marie Pédrot |
| 2018-05-30 | [api] Remove deprecated object from `Term` | Emilio Jesus Gallego Arias |
| 2018-05-17 | Split off Universes functions dealing with generating new universes. | Gaëtan Gilbert |
| 2018-03-06 | romega: get rid of EConstr.Unsafe | Pierre Letouzey |
| 2018-02-19 | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | Maxime Dénès |
| 2018-02-17 | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle |
| 2018-02-12 | [engine] Remove ghost parameter from `Proofview.Goal.t` | Emilio Jesus Gallego Arias |
| 2017-12-01 | Proper nametab handling of global universe names | Matthieu Sozeau |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès |
| 2017-11-23 | Recognizing Z in romega up to conversion. | Hugo Herbelin |
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias |
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | 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-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin |
| 2017-07-17 | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias |
| 2017-06-16 | romega: avoid potential slowdown when changing concl by reified version | Pierre Letouzey |
| 2017-06-12 | Merge PR#718: API cleanup: aliases | Maxime Dénès |
| 2017-06-10 | Remove remaining vo.itarget files (obsolete since PR #499) | Pierre Letouzey |
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík |
| 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-29 | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès |
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias |
| 2017-05-27 | [coqlib] Move `Coqlib` to `library/`. | Emilio Jesus Gallego Arias |
| 2017-05-27 | [coqlib] Deprecate redundant Coqlib functions. | Emilio Jesus Gallego Arias |
| 2017-05-24 | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey |
| 2017-05-22 | refl_omega: some code refactoring | Pierre Letouzey |
| 2017-05-22 | refl_omega.v: explicitely identify atom indexes and omega vars | Pierre Letouzey |
| 2017-05-22 | ReflOmegaCore: misc cleanup, <? instead of bgt, etc | 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 | ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple) | Pierre Letouzey |
| 2017-05-22 | ReflOmegaCore: comment, reorganize, permut some constructors, etc | Pierre Letouzey |
| 2017-05-22 | romega: add a tactic named unsafe_romega (for debugging, or bold users) | Pierre Letouzey |
| 2017-05-22 | romega: no more normalization trace, replaced by some Coq-side computation | Pierre Letouzey |
| 2017-05-22 | romega/const_omega : a few improvements (less try with, no gen equality) | Pierre Letouzey |
| 2017-05-22 | romega: use N instead of nat for Tvar | Pierre Letouzey |
| 2017-05-22 | romega: shorter trace (no more term lengths) | Pierre Letouzey |
| 2017-05-22 | refl_omega: refactoring of normalize_equation | Pierre Letouzey |
| 2017-05-22 | ReflOmegaCore: lots of dead code + a few refactored proofs | Pierre Letouzey |
| 2017-05-22 | romega: if it bugs again, at least do it with a short and quick error | Pierre Letouzey |
| 2017-05-22 | refl_omega: comment the lack of lifts when dealing with arrows | Pierre Letouzey |
