aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-02-06unsafe_type_of -> type_of in Pretyping.pretype_refGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Unification.applyHeadGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tacred.pattern_occsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-07[coercions] more precise type for coercion tracesMaxime Dénès
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-24[recordops] do not open GlobRefEnrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-18Merge PR #6090: Implement open recursion in the pretyperEnrico Tassi
2019-12-17Type pretyping is part of the open recursionPierre-Marie Pédrot
2019-12-17Exporting the open-recursion style API.Pierre-Marie Pédrot
2019-12-17Implementing open recursion in the pretyper.Pierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-11-26coercion functions are never called without a term to coerceGaëtan Gilbert
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
2019-10-18factorize or_var_mapAlexandre Moine
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-22Merge PR #9062: Delay the computation of frozen evars in legacy unification.Matthieu Sozeau
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:04:15 +0000