aboutsummaryrefslogtreecommitdiff
path: root/kernel/mod_subst.ml
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-07Canonical representation of kernel substitutions.Pierre-Marie Pédrot
2018-09-07Remove dead code in Mod_subst.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-09-20Fix #3948 Anomaly: unknown constant in Print AssumptionsMaxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-10-31Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)letouzey
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 2)letouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
2013-02-26Mod_subst: misc reformulationsletouzey
2013-02-19Mod_subst: an extra assertletouzey
2013-02-18Mod_subst: improve sharing during kn substitutionsletouzey
2013-01-27Slightly improving some debugging printing and error message for modules.herbelin
2012-12-18Modulification of mod_bound_idppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-02Remove some dead code in the vmletouzey
2012-09-25Fixing ocamldoc errorsppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-10-26Mod_subst: some simplifications, some more significant names to functions, etcletouzey
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-11Mod_subst: an unused functionletouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-08-01fixed bug 2580. Quick fix: copy emitcodes before patching itbarras
2011-02-24Mod_subst: improving sharing of subst_mpsletouzey
2011-02-23Some more simplification in Mod_substletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:51:06 +0000