aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
2020-10-14[build] [native] Don't assume installed native libraries are in custom output...Emilio Jesus Gallego Arias
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
2020-10-12Merge PR #13156: Store the resolver of required modules as functor parameters...coqbot-app[bot]
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-11Similarly remove the explicit graph argument in the ~evar conversion API.Pierre-Marie Pédrot
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-10-11Remove the compare_graph field from the conversion API.Pierre-Marie Pédrot
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
2020-10-09Store the resolver of required modules as functor parameters in safe_env.Pierre-Marie Pédrot
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-10-08Reroot primitive arrays on access (fix #12947).Guillaume Melquiond
2020-10-06Use OCaml floating-point operations on 64 bits archPierre Roux
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
2020-08-28Drop opaque bodies of abstracted definitions.Pierre-Marie Pédrot
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-18Fix subject reduction VS cumulative inductives and function etaGaëtan Gilbert
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-06Add a few comments about the code.Pierre-Marie Pédrot
2020-08-06Store the default instance in named_context_val.Pierre-Marie Pédrot
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-08Preserve delta-resolver at Module and Module Type starting.Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-06-17Use an efficient data structure for VM compilation indexing.Pierre-Marie Pédrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Cleanup: remove noisy "sec_" prefixes in section.mlGaëtan Gilbert
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-22Remove # keywords in PrimitivePierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:29:52 +0000