| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-04 | Fixing superflous newline in output of About when no parameter is renamed. | herbelin |
| 2011-11-21 | Renamig support added to "Arguments" | gareuselesinge |
| 2011-11-21 | New Arguments vernacular | gareuselesinge |
| 2011-10-11 | Various simplifications about constant_of_delta and mind_of_delta | letouzey |
| 2011-09-05 | Lib.node: merge OpenedModtype and OpenedModule, same for Closed... | letouzey |
| 2011-05-21 | Restore display of notation when printing an inductive such as sig | letouzey |
| 2011-05-11 | Print Module (Type) M now tries to print more details | letouzey |
| 2011-04-08 | Fixing multiple printing bugs with "Notation f x := ..." | herbelin |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-10-03 | Making display of various informations about constants more modular: | herbelin |
| 2010-10-03 | Fixed a little printing bug with "About" on an undefined constant. | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-26 | Applying François' patches about Canonical Projections (see #2302 and #2334). | herbelin |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-08-07 | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-07-15 | - Granted wish #2138 (support for local binders in syntax of Record fields). | herbelin |
| 2009-06-03 | Ensure the precondition of the partial function [list_chop] holds | msozeau |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-11-23 | Fixed bug #2006 (type constraint on Record was not taken into account) + | herbelin |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-07-25 | Correction d'une incohérence de typage des inductifs polymorphes: les | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-05-22 | Strategy commands are now exported | barras |
| 2008-05-21 | refined the conversion oracle | barras |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-15 | - Add "Global" modifier for instances inside sections with the usual | msozeau |
| 2008-04-12 | Document the new setoid rewrite tactic, and fix a few things while | msozeau |
| 2008-03-30 | Ajout d'abbréviations/notations paramétriques | herbelin |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-02-19 | added products and sorts as possible heads for canonical structures | corbinea |
| 2008-02-14 | Added default canonical structures (see example in test-suite) | corbinea |
| 2008-02-01 | Beaoucoup de changements dans la representation interne des modules. | soubiran |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
