aboutsummaryrefslogtreecommitdiff
path: root/theories/Program/Syntax.v
AgeCommit message (Expand)Author
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-04-08A module out of Program to have list notations (bug 2463)pboutill
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-10-03Using multiple lists of implicit arguments in Program for preservingherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-17Kill some useless dependencies (Bvector, Program.Syntax)letouzey
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-11- Resolve type class constraints before trying to find unresolvedmsozeau
2009-01-21- Better deal with commands inside section titles in latex output usingmsozeau
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau