| Commit message (Expand) | Author | Age |
... | |
| | | | * | | | | | | | Make install a single colon target for retro compatibility | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | enters coq_makefile2 | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | test suite for coq_makefile2 | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | coqdep: remove optimization making makefiles harder to write | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | ocamlfind: coqtop -config prints ocamlfind as found by ./configure | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | coqdep: set FOR_PACK variable for files that need to be packed | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | print_config: print COQ_SRC_SUBDIRS | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | Document --print-version in Usage | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | Put the list of Coq sources subdirectories in one place | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | Usage.print_config moved to Envars | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | CoqProject_file: document in API deprecated features | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | CoqProject_file: API and code cleanup (tuples -> records) | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | ide/project_fie.ml4: include standard banner with copyright | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | test suite for coq_makefile | Enrico Tassi | 2017-05-23 |
| | | | * | | | | | | | configure: -local set coqdoc destination dir to ./doc rather than "" | Enrico Tassi | 2017-05-23 |
| |_|_|/ / / / / / /
|/| | | | | | | | | |
|
| | | | | | | | * | | Bigint.euclid: clarify which sign convention is used | Pierre Letouzey | 2017-05-23 |
* | | | | | | | | | | Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit... | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ | Merge PR#659: Mention ./configure in INSTALL.doc | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#657: [test-suite] Add tests for goal printing. | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#646: Revised behavior on ill-formed identifiers | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#660: Change wrong bullet message. | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#518: Faster universe unification | Maxime Dénès | 2017-05-23 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | * | | | | | | | | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | 2017-05-23 |
| | | | | | | | * | | | | | | | | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias | 2017-05-23 |
| |_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | * | | 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 |
| | | | | | | | | | | | | * | | refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp) | Pierre Letouzey | 2017-05-22 |
| | | | | | | | | | | | | * | | ReflOmegaCore: discard useless cosntructor P_NOP | Pierre Letouzey | 2017-05-22 |
| | | | | | | | | | | | | * | | ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||]) | Pierre Letouzey | 2017-05-22 |
| |_|_|_|_|_|_|_|_|_|_|_|/ /
|/| | | | | | | | | | | | | |
|
| | | | | | | | | | * | | | | Compatibility fix while waiting for integration of Pierre Courtieu's PR #449. | Hugo Herbelin | 2017-05-22 |
| | | | | | | | | | * | | | | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin | 2017-05-22 |
| | | | | | | | | | * | | | | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | 2017-05-22 |
| |_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | |
|