aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2020-03-24Merge PR #11858: Rename Retypeops -> RelevanceopsPierre-Marie Pédrot
2020-03-23Merge PR #11867: Fix the computation of recursive principles with let-bindings.Enrico Tassi
2020-03-20Fix the computation of recursive principles with let-bindings.Pierre-Marie Pédrot
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-25Fix backtraces in conversion anomalies caught by Reductionops.Pierre-Marie Pédrot
2020-02-24Merge PR #11623: Deprecate unsafe_type_ofPierre-Marie Pédrot
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-18Deprecate unsafe_type_ofGaëtan Gilbert
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2020-02-11Reinforcing the role of type "typing_constraint".Hugo Herbelin
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence of...Pierre-Marie Pédrot
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
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-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
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-02-02Move kind_of_type from the kernel to ssr.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:55:25 +0000