aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/refl_omega.ml
Commit message (Expand)AuthorAge
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* romega: get rid of EConstr.UnsafeGravatar Pierre Letouzey2018-03-06
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* ROmega: division-aware ReflOmegaCore, allowing trace without termsGravatar Pierre Letouzey2017-05-24
* refl_omega: some code refactoringGravatar Pierre Letouzey2017-05-22
* refl_omega.v: explicitely identify atom indexes and omega varsGravatar Pierre Letouzey2017-05-22
* ROmega : O_STATE turned into a O_SUMGravatar Pierre Letouzey2017-05-22
* ROmega: less contructors in the final omega traceGravatar Pierre Letouzey2017-05-22
* ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTGravatar Pierre Letouzey2017-05-22
* romega: add a tactic named unsafe_romega (for debugging, or bold users)Gravatar Pierre Letouzey2017-05-22
* romega: no more normalization trace, replaced by some Coq-side computationGravatar Pierre Letouzey2017-05-22
* romega: use N instead of nat for TvarGravatar Pierre Letouzey2017-05-22
* romega: shorter trace (no more term lengths)Gravatar Pierre Letouzey2017-05-22
* refl_omega: refactoring of normalize_equationGravatar Pierre Letouzey2017-05-22
* refl_omega: comment the lack of lifts when dealing with arrowsGravatar Pierre Letouzey2017-05-22
* romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
* refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Gravatar Pierre Letouzey2017-05-22
* refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Gravatar Pierre Letouzey2017-05-22
* Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 02:43:17 +0000