aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Univs: Change intf of push_named_def to return the computed universeGravatar Matthieu Sozeau2015-10-02
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: forgot a substitution in mod_typing.Gravatar Matthieu Sozeau2015-10-02
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
* 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
* Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
* 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
* Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
* print universes when dumping bytecode.Gravatar Gregory Malecha2015-09-03
* Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
* Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
* Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
* Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
* 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
* Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
* Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
* 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
* 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
* Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
* Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
* Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
* Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* Fixing documentation (see Maxime's mail on coqdev, July 3).Gravatar Hugo Herbelin2015-07-05
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Fix convertibility of primitive projections for native_compute.Gravatar Maxime Dénès2015-07-03
* More robust pattern matching on structured constants in VM.Gravatar Maxime Dénès2015-07-02
* Display functions for primitive projections.Gravatar Maxime Dénès2015-07-02
* Further simplification of the graph traversal in Univ.Gravatar Pierre-Marie Pédrot2015-07-01
* Share prop/set values in sorts.ml.Gravatar Matthieu Sozeau2015-06-26
* BUGFIX: Three fixes for the price of 1 in sorts.ml:Gravatar Matthieu Sozeau2015-06-26
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-24
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-23
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:39:03 +0000