aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
|
* Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
| | | | Previously, the kernel was silently switching back to the standard conversion.
* Remove now useless exception handler in default conversion.Gravatar Maxime Dénès2015-10-15
|
* Fix detection of ties in oracle_order.Gravatar Guillaume Melquiond2015-10-15
| | | | | This commit has no impact, since l2r is always false in practice due to the definition of default_conv.
* Univs: inductives, remove unneeded testGravatar Matthieu Sozeau2015-10-14
|
* Temporary fix: kernel conversion needs to ignore l2r flag.Gravatar Maxime Dénès2015-10-14
| | | | | Stdlib does not compile when l2r flag is actually taken into account. We should investigate...
* Remove reference to default conversion function inside the kernel.Gravatar Maxime Dénès2015-10-14
|
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
| | | | | Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel.
* Remove unused infos structure in VM.Gravatar Maxime Dénès2015-10-14
| | | | Became unused after c47b205206d832430fa80a3386be80149e281d33.
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
|
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
| | | | direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
|
* Complete handling of primitive projections in VM.Gravatar Maxime Dénès2015-10-09
| | | | This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
| | | | | Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values.
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
| | | | Add a flag to disallow minimization to set
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | - "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.
* term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | | | 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.
* Univs: fix bug #4288, Print Sorted generated backward < constraints.Gravatar Matthieu Sozeau2015-10-05
|
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
| | | | | | | context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time.
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
| | | | | | 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.
* Univs: forgot a substitution in mod_typing.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
| | | | | For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: fix subtyping of polymorphic parameters.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: uncovered bug in strengthening of opaque polymorphic definitions.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: handle side-effects of futures correctly in kernel.Gravatar Matthieu Sozeau2015-10-02
|
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
| | | | | | Remove predicative flag and adapt to new invariant where every universe must be declared, ensuring it is >= Set, safe_repr is not necessary anymore.
* Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
| | | | declare new universes (e.g. with).
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
|
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
|
* Remove unused type_in_type field in safe_env.Gravatar Maxime Dénès2015-09-20
| | | | Was left over after Hugo's 9c732a5c878b.
* Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
| | | | | Substitution on bound modules was incorrectly extended without sequential composition.
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
| | | | | | | | | 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.
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
| | | | ADDMULDIVINT31 was missing pops in some cases
* print universes when dumping bytecode.Gravatar Gregory Malecha2015-09-03
|
* Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
| | | | | | | | | | | Hugo Herbelin proposed to modify directly the function "check_correct_par" to simplify commit c12b430 (see the pullrequest's discussion). Note that the constructor "LocalNonPar" has now three arguments (instead of two). In LocalNonPar (n,i,l) n denotes the position among real arguments (ie. ignoring letins), i is the rel index of the expecting argument in the context of parameters and l is the index of the inductive.
* Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
| | | | This is necessary for the patch for #4221 (817308ab5) to work.
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
|
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same.
* Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
| | | | | | The hash function exported by the interface ought to respect the equality. Therefore, we only use the syntactic hash for the hashconsing module while using the canonical hash in the API.
* Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
| | | | | | | | | | | compatible with a unique bound module name counter which is not synchronous with the backtracking). We changed hash-consing of kernel name pairs to a purely memory management issue, not trying to exploit logical properties such as "syntactically equal user names have syntactically same canonical names" (which is true in a given logical session, but not in memory, at least because of residual values after backtracking).
* Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
|
* a small amount of documentation on the virtual machine.Gravatar Gregory Malecha2015-07-23
|
* Fix incomplete pattern-matching.Gravatar Matthieu Sozeau2015-07-22
| | | | | I was not seeing the warning due to the 10 deprecation warnings before it...
* Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
| | | | | We were throwing away constraints from 'with Definition' in module type ascriptions.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:56:53 +0000