| Age | Commit message (Expand) | Author |
|---|
| 2017-06-01 | Merge PR#561: Improving the Name API | Maxime Dénès |
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin |
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin |
| 2017-05-30 | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin |
| 2017-05-30 | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin |
| 2017-05-30 | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès |
| 2017-05-29 | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès |
| 2017-05-28 | Merge PR#678: [coqlib] Move `Coqlib` to `library/`. | Maxime Dénès |
| 2017-05-28 | Fail on deprecated warning even for Ocaml > 4.02.3 | Gaëtan Gilbert |
| 2017-05-28 | Merge PR#675: [coqlib] Deprecate redundant Coqlib functions. | Maxime Dénès |
| 2017-05-27 | [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 | Exporting a few primitive tacticals as named Ltac definitions. | Pierre-Marie Pédrot |
| 2017-05-26 | Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso... | Maxime Dénès |
| 2017-05-25 | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès |
| 2017-05-25 | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès |
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias |
| 2017-05-24 | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey |
| 2017-05-24 | [option] Remove support for non-synchronous options. | 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 | 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-19 | Merge branch 'master' into ltac2-hooks | Pierre-Marie Pédrot |
| 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 |
