aboutsummaryrefslogtreecommitdiff
path: root/interp/impargs.ml
AgeCommit message (Expand)Author
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-13Implicit arguments: Fixing count of the position in compute_implicit_statuses.Hugo Herbelin
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Turn trailing implicit warning into an errorSimonBoulier
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-05-23Fixing typos - Part 2JPR
2019-05-18Merge PR #10134: Simplify impargsHugo Herbelin
2019-05-10Remove ref from some implicit_discharge_requestJasper Hugunin
2019-05-10Simplify dispose_implicitsJasper Hugunin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-18Merge PR #9589: Deprecate duplicated explicitation_eqEmilio Jesus Gallego Arias
2019-02-16Deprecated duplicated explicitation_eqJasper Hugunin
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-16Termops.iter_constr_with_full_binders = EConstr.iter_with_full_bindersGaëtan Gilbert
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-07-24Projections use index representationGaëtan Gilbert
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-05Refactor impargs code.Jasper Hugunin
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:59:24 +0000