aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
...
* 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.
* Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
| | | | | | | I was trying to be a bit too clever with not substituting the universe instance everywhere: the constructor type/inductive arity has to be instantiated before instantiate_params runs, which became true only for constructor types since my last commit.
* Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
|
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| | | | | | | | | | in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
* Native compiler: make non-fatal linking errors silent except in debug mode.Gravatar Maxime Dénès2015-07-10
|
* Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
| | | | Fixes #4139 (Not_found exception with Require in modules).
* Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
| | | | | Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/
* Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
| | | | | | | Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins.
* Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
| | | | | | | | | | Since Guillaume's, launching coqtop without -native-compiler and call native_compute would mean recompiling silently all dependencies, even if they had been precompiled (e.g. the stdlib). The new semantics is that -native-compiler disables separate compilation of the current library, but still tries to load precompiled dependencies. If loading fails when the flag is on, coqtop stays silent.
* Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| | | | | | | | | | | Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml.
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
| | | | | Missing universe substitutions of mind_params_ctxt when typechecking cases, which appeared only when let-ins were used.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 16:27:13 +0000