aboutsummaryrefslogtreecommitdiff
path: root/library/decls.ml
AgeCommit message (Expand)Author
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-04-29Merging Context and Sign.ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (library)ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-04-08Some dead code removal + cleanupsletouzey
2008-04-24Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840herbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:51:52 +0000