| Commit message (Expand) | Author | Age |
|---|
| * | Fixing multiple printing bugs with "Notation f x := ..." |  herbelin | 2011-04-08 |
| * | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks |  letouzey | 2011-04-03 |
| * | Change of nomenclature: rawconstr -> glob_constr |  glondu | 2010-12-23 |
| * | 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-10-03 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Applying François' patches about Canonical Projections (see #2302 and #2334). | herbelin | 2010-06-26 |
| * | Fixing spelling: pr_coma -> pr_comma | herbelin | 2010-06-12 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin | 2009-11-11 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... |  msozeau | 2009-10-28 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
| * | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin | 2009-08-07 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | - Granted wish #2138 (support for local binders in syntax of Record fields). | herbelin | 2009-07-15 |
| * | Ensure the precondition of the partial function [list_chop] holds | msozeau | 2009-06-03 |
| * | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin | 2008-12-31 |
| * | Fixed bug #2006 (type constraint on Record was not taken into account) + | herbelin | 2008-11-23 |
| * | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin | 2008-09-02 |
| * | - New auto hints for transparency/opacity control, not bound to | msozeau | 2008-08-22 |
| * | Correction d'une incohérence de typage des inductifs polymorphes: les | herbelin | 2008-07-25 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | Strategy commands are now exported |  barras | 2008-05-22 |
| * | refined the conversion oracle | barras | 2008-05-21 |
| * | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
| * | - Add "Global" modifier for instances inside sections with the usual | msozeau | 2008-04-15 |
| * | Document the new setoid rewrite tactic, and fix a few things while | msozeau | 2008-04-12 |
| * | Ajout d'abbréviations/notations paramétriques | herbelin | 2008-03-30 |
| * | Do another pass on the typeclasses code. Correct globalization of class | msozeau | 2008-03-19 |
| * | added products and sorts as possible heads for canonical structures |  corbinea | 2008-02-19 |
| * | Added default canonical structures (see example in test-suite) | corbinea | 2008-02-14 |
| * | Beaoucoup de changements dans la representation interne des modules. | soubiran | 2008-02-01 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Correction ordre d'affichage des champs des Record | herbelin | 2007-12-14 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options |  aspiwack | 2007-12-06 |
| * | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
| * | Correction de quelques défauts d'affichage (notations sous "as" pour | herbelin | 2007-10-05 |
| * | Réaffichage des Structure/Record sous la forme Record | herbelin | 2007-05-28 |
| * | Nouveaux changements autour des implicites (notamment suite à | herbelin | 2007-05-06 |
| * | Merge from Lionel Elie Mamane's private branch: |  lmamane | 2007-01-10 |
| * | Suite ajout option -output-context | herbelin | 2006-12-08 |
| * | Ajout d'une option -output-context qui affiche le contexte en CCI pur à la | herbelin | 2006-12-08 |
| * | Compatibilité du polymorphisme de constantes avec les sections. | herbelin | 2006-10-29 |
| * | Ajout option Set Printing Universes et amélioration affichage des univers | herbelin | 2006-10-28 |
| * | Déplacement surround dans util.ml et parenthésage des déclarations | herbelin | 2006-09-23 |
| * | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
herbelin
letouzey
glondu
msozeau
soubiran
barras
corbinea
aspiwack
lmamane