| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| Previously, the kernel was silently switching back to the standard conversion. | |||
| 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 | Add a field in `constant_body` to track constant whose well-foundedness is ↵ | Arnaud Spiwack | |
| assumed. | |||
| 2015-09-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-25 | Propagate `Guarded` flag from syntax to kernel. | Arnaud Spiwack | |
| The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |