aboutsummaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
AgeCommit message (Expand)Author
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
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-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-11-26coercion functions are never called without a term to coerceGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:42:12 +0000