| Age | Commit message (Expand) | Author |
|---|
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias |
| 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 | 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 | 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: 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 | 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-04-24 | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot |
| 2017-02-14 | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot |
| 2017-02-14 | Tactics API using EConstr. | Pierre-Marie Pédrot |
| 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-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-16 | Put the "generalize" tactic in the monad. | 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-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList.index is now cList.index_f, same for index0 | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 11) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-06-01 | Cleaning Pp.ppnl use | ppedrot |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-07-29 | Refl_omega: replaced generic = on constr by eq_constr | puech |
| 2011-07-29 | Refl_omega: replaced some generic = on constr by eq_constr | puech |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
