aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:25:42 +0000