| Age | Commit message (Expand) | Author |
|---|
| 2015-10-25 | Minor module cleanup : error HigherOrderInclude was never happening | Pierre Letouzey |
| 2015-10-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin |
| 2015-10-18 | Adding a function to mirror decompose_prod_n_assum in that it counts let-ins, | Hugo Herbelin |
| 2015-10-16 | Remove left2right reference from the kernel. | Maxime Dénès |
| 2015-10-15 | Avoid dependency of the pretyper on C code. | Maxime Dénès |
| 2015-10-15 | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-15 | Warn user when bytecode compilation fails. | Maxime Dénès |
| 2015-10-15 | Remove now useless exception handler in default conversion. | Maxime Dénès |
| 2015-10-15 | Fix detection of ties in oracle_order. | Guillaume Melquiond |
| 2015-10-14 | Univs: inductives, remove unneeded test | Matthieu Sozeau |
| 2015-10-14 | Temporary fix: kernel conversion needs to ignore l2r flag. | Maxime Dénès |
| 2015-10-14 | Remove reference to default conversion function inside the kernel. | Maxime Dénès |
| 2015-10-14 | Remove -vm flag of coqtop. | Maxime Dénès |
| 2015-10-14 | Remove unused infos structure in VM. | Maxime Dénès |
| 2015-10-14 | Make interpreter of PROJ simpler by not using the stack. | Guillaume Melquiond |
| 2015-10-14 | Remove some unused variables. | Guillaume Melquiond |
| 2015-10-14 | Fix some typos. | Guillaume Melquiond |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-10-12 | Univs: be more restrictive for template polymorphic constants: only | Matthieu Sozeau |
| 2015-10-12 | Gather VM tags in Cbytecodes. | Maxime Dénès |
| 2015-10-09 | Complete handling of primitive projections in VM. | Maxime Dénès |
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-08 | term_typing: strengthen discharging code | Enrico Tassi |
| 2015-10-05 | Univs: fix bug #4288, Print Sorted generated backward < constraints. | Matthieu Sozeau |
| 2015-10-02 | Univs: Change intf of push_named_def to return the computed universe | Matthieu Sozeau |
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau |
| 2015-10-02 | Univs: forgot a substitution in mod_typing. | Matthieu Sozeau |
| 2015-10-02 | Univs: correct handling of with in modules | Matthieu Sozeau |
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau |
| 2015-10-02 | Univs: fix subtyping of polymorphic parameters. | Matthieu Sozeau |
| 2015-10-02 | Univs: uncovered bug in strengthening of opaque polymorphic definitions. | Matthieu Sozeau |
| 2015-10-02 | Univs: handle side-effects of futures correctly in kernel. | Matthieu Sozeau |
| 2015-10-02 | Univs (kernel) adapt to new invariants | Matthieu Sozeau |
| 2015-10-02 | Univs: module constraints move to universe contexts as they might | Matthieu Sozeau |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau |
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau |
| 2015-09-20 | Remove unused type_in_type field in safe_env. | Maxime Dénès |
| 2015-09-20 | Fix #3948 Anomaly: unknown constant in Print Assumptions | Maxime Dénès |
| 2015-09-06 | Fix a bug in 31 bit arithmetic, leading to failing conversion tests. | Maxime Dénès |
| 2015-09-06 | Fixed critical bug in 31 bit arithmetic of VM | Catalin Hritcu |
| 2015-09-03 | print universes when dumping bytecode. | Gregory Malecha |
| 2015-09-03 | Implementing Herbelin's fix for the "NonPar" bug | mlasson |
| 2015-08-02 | Fixing pop_rel_context. | Hugo Herbelin |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Fixing pop_rel_context | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
