aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
Commit message (Expand)AuthorAge
* [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
* Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\
* | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| * Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Deprecate redundant Coqlib functions.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
* ReflOmegaCore: misc cleanup, <? instead of bgt, etcGravatar 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
* ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)Gravatar Pierre Letouzey2017-05-22
* ReflOmegaCore: comment, reorganize, permut some constructors, etcGravatar 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/const_omega : a few improvements (less try with, no gen equality)Gravatar 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
* ReflOmegaCore: lots of dead code + a few refactored proofsGravatar Pierre Letouzey2017-05-22
* romega: if it bugs again, at least do it with a short and quick errorGravatar 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
* ReflOmegaCore: discard useless cosntructor P_NOPGravatar Pierre Letouzey2017-05-22
* ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Gravatar Pierre Letouzey2017-05-22
* Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* Reduce warning noise when compiling the standard library.Gravatar Guillaume Melquiond2016-08-09
* 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
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17