aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
Commit message (Expand)AuthorAge
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\
| * Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
|/
* [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
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* [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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 17:05:53 +0000