| Commit message (Expand) | Author | Age |
... | |
| | | * | | | | | | extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME... | Matej Kosik | 2017-06-01 |
| |_|/ / / / / /
|/| | | | | | | |
|
| | | | | | * | | Fix bug #5019 (looping zify on dependent types) | Jason Gross | 2017-06-01 |
| | | | * | | | | [printing] Remove duplicated printing function. | Emilio Jesus Gallego Arias | 2017-06-01 |
| |_|_|/ / / /
|/| | | | | | |
|
| | | * | | | | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin | 2017-05-31 |
| | | | * | | | Factorizing interp_gen through a function interpreting glob_constr. | Hugo Herbelin | 2017-05-31 |
| | | | * | | | Splitting interp_open_constr into two variants, with or without type classes. | Hugo Herbelin | 2017-05-31 |
| | | |/ / / |
|
| * | / / / | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | 2017-05-31 |
| | |/ / /
| |/| | | |
|
| | | | * | Makefile: no bytecode compilation in make world, see make byte instead | Pierre Letouzey | 2017-05-30 |
| | |_|/
| |/| | |
|
* | | | | Support for using type information to infer more precise evar sources. | Hugo Herbelin | 2017-05-30 |
* | | | | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin | 2017-05-30 |
* | | | | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin | 2017-05-30 |
|/ / / |
|
* | | | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès | 2017-05-30 |
|\ \ \ |
|
| | | * | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey | 2017-05-29 |
| | * | | Ltac cleanup: no more constr_of_global calls | Matthieu Sozeau | 2017-05-29 |
| | * | | Equality cleanup: remove constr_of_global | Matthieu Sozeau | 2017-05-29 |
| | * | | Cleanup: removal of constr_of_global. | Matthieu Sozeau | 2017-05-29 |
| |/ /
|/| | |
|
* | | | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès | 2017-05-29 |
|\ \ \ |
|
* \ \ \ | Merge PR#678: [coqlib] Move `Coqlib` to `library/`. | Maxime Dénès | 2017-05-28 |
|\ \ \ \ |
|
| | | * | | Fail on deprecated warning even for Ocaml > 4.02.3 | Gaëtan Gilbert | 2017-05-28 |
* | | | | | Merge PR#675: [coqlib] Deprecate redundant Coqlib functions. | Maxime Dénès | 2017-05-28 |
|\ \ \ \ \ |
|
| | | * | | | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | 2017-05-27 |
| | | |/ / |
|
| | * / / | [coqlib] Move `Coqlib` to `library/`. | Emilio Jesus Gallego Arias | 2017-05-27 |
| |/ / / |
|
| * / / | [coqlib] Deprecate redundant Coqlib functions. | Emilio Jesus Gallego Arias | 2017-05-27 |
| |/ / |
|
* / / | Exporting a few primitive tacticals as named Ltac definitions. | Pierre-Marie Pédrot | 2017-05-27 |
|/ / |
|
* | | Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso... | Maxime Dénès | 2017-05-26 |
|\ \ |
|
* \ \ | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | 2017-05-25 |
|\ \ \ |
|
* \ \ \ | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès | 2017-05-25 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | 2017-05-25 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | 2017-05-24 |
|\ \ \ \ \ \ |
|
| | | | | * | | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey | 2017-05-24 |
| | * | | | | | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | 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 |
| | | | * | | ReflOmegaCore: misc cleanup, <? instead of bgt, etc | 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 |
| | | | * | | ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple) | Pierre Letouzey | 2017-05-22 |
| | | | * | | ReflOmegaCore: comment, reorganize, permut some constructors, etc | 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/const_omega : a few improvements (less try with, no gen equality) | 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 |
| | | | * | | ReflOmegaCore: lots of dead code + a few refactored proofs | Pierre Letouzey | 2017-05-22 |
| | | | * | | romega: if it bugs again, at least do it with a short and quick error | 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 |