| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-15 | Remove now useless exception handler in default conversion. | Maxime Dénès | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-15 | Fix detection of ties in oracle_order. | Guillaume Melquiond | |
| This commit has no impact, since l2r is always false in practice due to the definition of default_conv. | |||
| 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 | |
| Stdlib does not compile when l2r flag is actually taken into account. We should investigate... | |||
| 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 | |
| Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel. | |||
| 2015-10-14 | Remove unused infos structure in VM. | Maxime Dénès | |
| Became unused after c47b205206d832430fa80a3386be80149e281d33. | |||
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-12 | Univs: be more restrictive for template polymorphic constants: only | Matthieu Sozeau | |
| direct aliases are ok, and indices should not be made polymorphic. Fixes NFix. | |||
| 2015-10-12 | Gather VM tags in Cbytecodes. | Maxime Dénès | |
| 2015-10-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-09 | Complete handling of primitive projections in VM. | Maxime Dénès | |
| This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1 | |||
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau | |
| Add a flag to disallow minimization to set | |||
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | |
| - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. | |||
| 2015-10-08 | term_typing: strengthen discharging code | Enrico Tassi | |
| Given the way Lib.extract_hyps is coded if the const_hyps field of a constant declaration contains a named_context that does not have the same order of the one in Environment.env, discharging is broken (as in some section variables are not discharged). If const_hyps is computed by the kernel, then the order is correct by construction. If such list is provided by the user, the order is not granted. We now systematically sort the list of user provided section hyps. The code of Proof using is building the named_context in the right order, but the API was not enforcing/checking it. Now it does. | |||
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | |
| 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. | |||
| 2015-10-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-05 | Univs: fix bug #4288, Print Sorted generated backward < constraints. | Matthieu Sozeau | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-02 | Univs: Change intf of push_named_def to return the computed universe | Matthieu Sozeau | |
| context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. | |||
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau | |
| According to their polymorphic/non-polymorphic status, which imply that universe variables introduced with it are assumed to be >= or > Set respectively in the following definitions. | |||
| 2015-10-02 | Univs: forgot a substitution in mod_typing. | Matthieu Sozeau | |
| 2015-10-02 | Univs: correct handling of with in modules | Matthieu Sozeau | |
| For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294 | |||
| 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 | |
| Remove predicative flag and adapt to new invariant where every universe must be declared, ensuring it is >= Set, safe_repr is not necessary anymore. | |||
| 2015-10-02 | Univs: module constraints move to universe contexts as they might | Matthieu Sozeau | |
| declare new universes (e.g. with). | |||
| 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-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-20 | Remove unused type_in_type field in safe_env. | Maxime Dénès | |
| Was left over after Hugo's 9c732a5c878b. | |||
| 2015-09-20 | Fix #3948 Anomaly: unknown constant in Print Assumptions | Maxime Dénès | |
| Substitution on bound modules was incorrectly extended without sequential composition. | |||
| 2015-09-20 | Better debug printers for module paths. | Maxime Dénès | |
| Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now. | |||
| 2015-09-14 | Remove dead code in lazy reduction machine. | Maxime Dénès | |
| 2015-09-10 | Assertion checking that invariant enforced by 0f8d1b92 always holds. | Maxime Dénès | |
| When reifying a 31-bit integer after a VM computation, we check that no bit outside the 31 LSB is set to 1. | |||
| 2015-09-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-06 | Output a warning when conversion compilation failed. | Maxime Dénès | |
| Previously, the kernel would silently fall back to standard conversion. | |||
| 2015-09-06 | Fix a bug in 31 bit arithmetic, leading to failing conversion tests. | Maxime Dénès | |
| On 64 bits architectures, integers could have some of their 32 msb set to 1 internally in the VM. When read back to a Coq term, this was not observable. But an equality test would fail. From the user point of view, the symptom was that vm_compute; reflexivity would succeed but the subsequent Qed would fail. Bug reported by Tahina Ramananandro. | |||
| 2015-09-06 | Fixed critical bug in 31 bit arithmetic of VM | Catalin Hritcu | |
| ADDMULDIVINT31 was missing pops in some cases | |||
| 2015-09-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-03 | print universes when dumping bytecode. | Gregory Malecha | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |