| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-25 | Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331) | Pierre Letouzey | |
| 2015-10-25 | Minor module cleanup : error HigherOrderInclude was never happening | Pierre Letouzey | |
| When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. | |||
| 2015-10-22 | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | |
| Was introduced in b06d3badb (15 Jul 2015). | |||
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | |
| to compensate decompose_lam_n_assum which does not count let-ins. Any idea on a uniform and clear naming scheme for this kind of decomposition functions? | |||
| 2015-10-16 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-10-16 | Hashcons bytecode generated by the VM. | Pierre-Marie Pédrot | |
| 2015-10-16 | Exporting a purely functional interface to bytecode patching. | Pierre-Marie Pédrot | |
| 2015-10-16 | Remove left2right reference from the kernel. | Maxime Dénès | |
| Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable. | |||
| 2015-10-15 | Avoid dependency of the pretyper on C code. | Maxime Dénès | |
| Using the same hack as in the kernel: VM conversion is a reference to a function, updated when modules using C code are actually linked. This hack should one day go away, but always linking C code may produce some other trouble (with the OCaml debugger for instance), so better be safe for now. | |||
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |