| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Reduce warning noise when compiling the standard library. |  Guillaume Melquiond | 2016-08-09 |
| * | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
| * | Compilation via pack for plugins of the stdlib | Pierre Letouzey | 2016-06-08 |
| * | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
| * | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
| * | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot | 2016-05-16 |
| * | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
| * | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot | 2016-03-17 |
| * | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot | 2016-03-04 |
| * | Getting rid of the "<:tactic< ... >>" quotations. | Pierre-Marie Pédrot | 2016-02-24 |
| * | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot | 2016-02-15 |
| * | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
| * | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
| * | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
Maxime Dénès
Emilio Jesus Gallego Arias
Pierre Letouzey
Pierre-Marie Pédrot
Guillaume Melquiond