| Commit message (Expand) | Author | Age |
|---|
| * | Proper nametab handling of global universe names |  Matthieu Sozeau | 2017-12-01 |
| * | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion |  Maxime Dénès | 2017-11-24 |
| |\ |
|
| | * | Recognizing Z in romega up to conversion. |  Hugo Herbelin | 2017-11-23 |
| * | | [api] Deprecate Term destructors, move to Constr |  Emilio Jesus Gallego Arias | 2017-11-22 |
| |/ |
|
| * | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | 2017-11-21 |
| * | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| * | romega: takes advantage of context variables with body |  Pierre Letouzey | 2017-10-05 |
| * | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | 2017-08-21 |
| * | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
| * | romega: avoid potential slowdown when changing concl by reified version | Pierre Letouzey | 2017-06-16 |
| * | Merge PR#718: API cleanup: aliases | Maxime Dénès | 2017-06-12 |
| |\ |
|
| * | | 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-10 |
| |/ |
|
| * | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 |
| * | Remove the Sigma (monotonous state) API. | Maxime Dénès | 2017-06-06 |
| * | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès | 2017-05-29 |
| |\ |
|
| | * | [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-27 |
| |/ |
|
| * | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey | 2017-05-24 |
| * | 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 | 2017-05-22 |
| * | romega: discard constructor D_mono (shorter trace + fix a bug) | Pierre Letouzey | 2017-05-22 |
| * | refl_omega: more refactoring (e.g. IntSets instead of sorted lists) | Pierre Letouzey | 2017-05-22 |
| * | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp) | Pierre Letouzey | 2017-05-22 |
| * | ReflOmegaCore: discard useless cosntructor P_NOP | Pierre Letouzey | 2017-05-22 |
| * | ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||]) | Pierre Letouzey | 2017-05-22 |
| * | Removing trivial compatibility layer in refl_omega. |  Pierre-Marie Pédrot | 2017-04-24 |
| * | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
| |\ |
|
| | * | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | 2017-02-17 |
| * | | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
| * | | Reductionops now return EConstrs. | Pierre-Marie Pédrot | 2017-02-14 |
| * | | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| * | | Tacmach API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
| |/ |
|
| * | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot | 2016-09-21 |
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Pierre Letouzey
Matej Košík
Pierre-Marie Pédrot