| Commit message (Expand) | Author | Age |
* | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 |
* | Remove the Sigma (monotonous state) API. | Maxime Dénès | 2017-06-06 |
* | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | 2017-05-27 |
* | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey | 2017-05-24 |
* | 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-05-22 |
* | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot | 2017-04-24 |
* | Removing various compatibility layers of tactics. | Pierre-Marie Pédrot | 2017-02-14 |
* | Tactics API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | Compilation via pack for plugins of the stdlib | Pierre Letouzey | 2016-06-08 |
* | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
* | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot | 2016-05-16 |
* | Moving conversion functions to the new tactic API. | Pierre-Marie Pédrot | 2016-02-15 |
* | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin | 2014-12-07 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau | 2014-06-23 |
* | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
* | 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-10-23 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | 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 | 2013-03-13 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | More cleaning on Utils and CList. Some parts of the code being | ppedrot | 2012-09-17 |
* | 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-09-14 |
* | Cleaning Pp.ppnl use | ppedrot | 2012-06-01 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Refl_omega: replaced generic = on constr by eq_constr | puech | 2011-07-29 |
* | Refl_omega: replaced some generic = on constr by eq_constr | puech | 2011-07-29 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey | 2009-03-20 |