aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Document the signatures of quotient names in the API.Pierre-Marie Pédrot
2020-10-21Introduce the missing dual name quotient modules in Environ.Pierre-Marie Pédrot
2020-10-21Code factorization in Names.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-21Introduce a dummy name quotient API.Pierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:04:47 +0000