aboutsummaryrefslogtreecommitdiff
path: root/plugins/romega/refl_omega.ml
AgeCommit message (Expand)Author
2018-09-25Remove romegaVincent Laporte
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-03-06romega: get rid of EConstr.UnsafePierre Letouzey
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24ROmega: division-aware ReflOmegaCore, allowing trace without termsPierre Letouzey
2017-05-22refl_omega: some code refactoringPierre Letouzey
2017-05-22refl_omega.v: explicitely identify atom indexes and omega varsPierre Letouzey
2017-05-22ROmega : O_STATE turned into a O_SUMPierre Letouzey
2017-05-22ROmega: less contructors in the final omega tracePierre Letouzey
2017-05-22ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTPierre Letouzey
2017-05-22romega: add a tactic named unsafe_romega (for debugging, or bold users)Pierre Letouzey
2017-05-22romega: no more normalization trace, replaced by some Coq-side computationPierre Letouzey
2017-05-22romega: use N instead of nat for TvarPierre Letouzey
2017-05-22romega: shorter trace (no more term lengths)Pierre Letouzey
2017-05-22refl_omega: refactoring of normalize_equationPierre Letouzey
2017-05-22refl_omega: comment the lack of lifts when dealing with arrowsPierre Letouzey
2017-05-22romega: discard constructor D_mono (shorter trace + fix a bug)Pierre Letouzey
2017-05-22refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Pierre Letouzey
2017-05-22refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Pierre Letouzey
2017-04-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 13:45:11 +0000