aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.mli
Commit message (Expand)AuthorAge
* Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix #3948 Anomaly: unknown constant in Print AssumptionsGravatar Maxime Dénès2015-09-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Updating headers.Gravatar herbelin2012-08-08
* Mod_subst: some simplifications, some more significant names to functions, etcGravatar letouzey2011-10-26
* Mod_subst: an unused functionGravatar letouzey2011-10-11
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* fixed bug 2580. Quick fix: copy emitcodes before patching itGravatar barras2011-08-01
* Mod_subst: improving sharing of subst_mpsGravatar letouzey2011-02-24
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* correction bug 1839Gravatar soubiran2008-04-25
* Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...Gravatar soubiran2008-03-26
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* HUGE COMMITGravatar sacerdot2005-01-03
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 05:54:36 +0000