aboutsummaryrefslogtreecommitdiff
path: root/toplevel/class.mli
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-07-16Nouvelle en-têteherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-05GROS COMMIT:barras
2001-07-05Débogage discharge des coercions; nettoyageherbelin
2001-03-15entetesfilliatr
2001-01-27make docherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-23Informations inutilesherbelin
2000-11-20Mieux à sa place dans toplevelherbelin
2000-01-11Ajout de Recordherbelin
2000-01-07Déplacement non-affichage des coercions dans termastherbelin
1999-12-13documentation interfacesfilliatr
1999-12-02Version initialeherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:21:02 +0000