aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Term_typing: remove unused argument to internal function.Gravatar Gaëtan Gilbert2018-07-03
* Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
* Indtypes: remove unused is_unit.Gravatar Gaëtan Gilbert2018-07-03
* Subtyping.check_constant: remove unused module path argument.Gravatar Gaëtan Gilbert2018-07-03
* Inductive.extract_stack,filter_stack_domain: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
* Nativecode compile_mind, compile_mind_field: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
* Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
* Modops.add_retroknowledge: remove unused argument.Gravatar Gaëtan Gilbert2018-07-03
* Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\
* | Deprecate Environ.retroknowledge function in favor of the projectionGravatar Gaëtan Gilbert2018-06-28
* | [env.env_rel_context.env_rel_ctx] -> [rel_context env]Gravatar Gaëtan Gilbert2018-06-28
* | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
* | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/|
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
| | * Test file for #7723Gravatar Maxime Dénès2018-06-27
| | * Fix #7723: vm_compute segfaults with universe polymorphismGravatar Maxime Dénès2018-06-27
| |/ |/|
* | Merge PR #7919: Fix equality check on global names from native compute.Gravatar Maxime Dénès2018-06-26
|\ \
| | * Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |/ |/|
* | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Gravatar Matthieu Sozeau2018-06-25
|\ \
| | * Fix equality check on global names from native compute.Gravatar Pierre-Marie Pédrot2018-06-25
| |/ |/|
* | Merge PR #7772: [native_compute] Delay computations with toplevel matchGravatar Pierre-Marie Pédrot2018-06-24
|\ \
* \ \ Merge PR #7614: Simplify the code that handles trust of side-effects in kerne...Gravatar Maxime Dénès2018-06-23
|\ \ \
* | | | Adapt the kernel to generate proper data for mutual records.Gravatar Pierre-Marie Pédrot2018-06-23
* | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* | | | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
* | | | Merge PR #7715: Simplify the cooking of primitive projections.Gravatar Maxime Dénès2018-06-23
|\ \ \ \
* \ \ \ \ Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Gravatar Maxime Dénès2018-06-22
|\ \ \ \ \
| | | | | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| | | | | * Define and use UGraph.enforce_leq_alg for subtyping inferenceGravatar Gaëtan Gilbert2018-06-22
| | | | | * Fix Univ.enforce_leq dropped constraints when algebraic on the rightGravatar Gaëtan Gilbert2018-06-19
| |_|_|_|/ |/| | | |
* | | | | Merge PR #7841: Remove CanaryGravatar Pierre-Marie Pédrot2018-06-19
|\ \ \ \ \
| * | | | | Remove Canary.Gravatar whitequark2018-06-18
* | | | | | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | | | | | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | | | | | Remove special declaration of primitive projections in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | | | | | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/ / / / /
| * / / / Faster and cleaner fconstr-to-constr conversion function.Gravatar Pierre-Marie Pédrot2018-06-17
|/ / / /
* | | | Merge PR #7635: Define rec_declaration in terms of prec_declaration.Gravatar Maxime Dénès2018-06-17
|\ \ \ \
* \ \ \ \ Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Gravatar Maxime Dénès2018-06-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7677: [api] Remove MisctypesGravatar Pierre-Marie Pédrot2018-06-13
|\ \ \ \ \ \
| * | | | | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | | | | | [VM] Rename reloc -> cenvGravatar Maxime Dénès2018-06-12
|/ / / / / /
| | | * / / Simplify the cooking of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-11
| |_|/ / / |/| | | |
| | | | * [native_compute] Delay computations with toplevel matchGravatar Maxime Dénès2018-06-11
* | | | | [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
| |_|_|/ |/| | |
| * | | Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
|/ / /
| * | Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
* | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
* | | Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
|/ /