| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 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-04-24 | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot |
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès |
| 2017-02-17 | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot |
| 2017-02-14 | 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 |
| 2016-09-21 | Merging Stdarg and Constrarg. | Pierre-Marie Pédrot |
| 2016-08-09 | Reduce warning noise when compiling the standard library. | Guillaume Melquiond |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-08 | Compilation via pack for plugins of the stdlib | Pierre Letouzey |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot |
| 2016-03-17 | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot |
| 2016-03-04 | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot |
| 2016-02-24 | Getting rid of the "<:tactic< ... >>" quotations. | Pierre-Marie Pédrot |
| 2016-02-15 | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | Clean up a comment in plugins/romega/ReflOmegaCore | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
