| Age | Commit message (Expand) | Author |
|---|
| 2017-05-23 | Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit... | Maxime Dénès |
| 2017-05-23 | Merge PR#659: Mention ./configure in INSTALL.doc | Maxime Dénès |
| 2017-05-23 | Merge PR#657: [test-suite] Add tests for goal printing. | Maxime Dénès |
| 2017-05-23 | Merge PR#646: Revised behavior on ill-formed identifiers | Maxime Dénès |
| 2017-05-23 | Merge PR#660: Change wrong bullet message. | Maxime Dénès |
| 2017-05-23 | Merge PR#518: Faster universe unification | Maxime Dénès |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias |
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias |
| 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-22 | Compatibility fix while waiting for integration of Pierre Courtieu's PR #449. | Hugo Herbelin |
| 2017-05-22 | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin |
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin |
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin |
| 2017-05-20 | Deprecate -nodoc. | Théo Zimmermann |
| 2017-05-20 | [coqdoc] Add keywords in bug 2884. | Emilio Jesus Gallego Arias |
| 2017-05-20 | Change wrong bullet message. | Théo Zimmermann |
| 2017-05-20 | Revised behavior on ill-formed identifiers. | Hugo Herbelin |
| 2017-05-20 | Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890). | Maxime Dénès |
| 2017-05-20 | Mention ./configure in INSTALL.doc | Théo Zimmermann |
| 2017-05-20 | Merge PR#654: Travis: do not cache opam logs (+prettier spacing) | Maxime Dénès |
| 2017-05-20 | Merge PR#643: [ide] Disable `print_ast` call. | Maxime Dénès |
| 2017-05-20 | Merge PR#474: A fix for #5390 (a useful error on used introduction names was ... | Maxime Dénès |
| 2017-05-20 | [test-suite] Add tests for goal printing. | Emilio Jesus Gallego Arias |
| 2017-05-20 | Merge PR#627: Obligations shrinking: shrink abstraction too | Maxime Dénès |
| 2017-05-20 | Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) | Maxime Dénès |
| 2017-05-20 | Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el | Maxime Dénès |
| 2017-05-20 | Merge PR#649: Fix a typo | Maxime Dénès |
| 2017-05-20 | Merge PR#651: Re-adding explicit dependency of misc universe test into all_st... | Maxime Dénès |
| 2017-05-20 | Merge PR#640: [toplevel] Restore 8.6 goal printing behavior. | Maxime Dénès |
