| Age | Commit message (Expand) | Author |
|---|
| 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-05-18 | Add .dir-locals.el to plugins | Jason Gross |
| 2017-05-17 | Merge PR#633: An extension of EXTEND and notations to make standard parsing t... | Maxime Dénès |
| 2017-05-17 | Merge PR#607: Make congruence reuse discriminate instead of rolling its own. | Maxime Dénès |
| 2017-05-16 | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | Hugo Herbelin |
| 2017-05-16 | Adding support for using grammar entries returning no value in EXTEND. | Hugo Herbelin |
| 2017-05-13 | Typo in a comment of plugin Quote. | Hugo Herbelin |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès |
| 2017-05-09 | Merge PR#612: Set Ltac Batch Debug | Maxime Dénès |
| 2017-05-09 | Prevent user-defined ring morphisms from ever being evaluated. | Guillaume Melquiond |
| 2017-05-04 | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat... | Hugo Herbelin |
| 2017-05-03 | Make congruence reuse discriminate instead of rolling its own. | Gaetan Gilbert |
| 2017-04-27 | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert |
| 2017-04-27 | Micromega: do not use Filename.temp_dir_path, remove unused values | Gaetan Gilbert |
| 2017-04-27 | Remove unused constructors | Gaetan Gilbert |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert |
| 2017-04-27 | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or | Gaetan Gilbert |
| 2017-04-27 | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum | Gaetan Gilbert |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert |
| 2017-04-27 | Remove unused [rec] keywords | Gaetan Gilbert |
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross |
| 2017-04-25 | Merge PR#578: Fix nsatz not recognizing real literals. | Maxime Dénès |
| 2017-04-24 | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot |
| 2017-04-24 | Porting the firstorder plugin to the new tactic API. | Pierre-Marie Pédrot |
| 2017-04-24 | Removing tactic compatibility layer in congruence. | Pierre-Marie Pédrot |
