index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
class.ml
Commit message (
Expand
)
Author
Age
*
More uniformisation in Pp.warn functions.
ppedrot
2012-05-30
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-05-29
*
Relax uniform inheritance condition
gareuselesinge
2012-04-05
*
Noise for nothing
pboutill
2012-03-02
*
Proof using ...
gareuselesinge
2011-12-12
*
Class: generic equality on constr replaced by destructors
puech
2011-07-29
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
An automatic substitution of scope at functor application
letouzey
2011-02-11
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Applying François' patch fixing grammar of uniform inheritance condition mes...
herbelin
2010-06-12
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about
herbelin
2008-09-02
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Correction bug 1841 (identificateurs incorrects avec Subclass)
herbelin
2008-06-10
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Complétion commit précédent
herbelin
2004-11-29
*
Réduire pour trouver l'arité d'une classe
herbelin
2004-11-26
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...
herbelin
2004-06-02
*
test de conversion laissait echapper exception NotConvertible
barras
2004-05-14
*
MAJ messages d'erreurs en accord avec la doc
herbelin
2003-12-20
*
Déplacement d'un morceau de Declare
herbelin
2003-09-12
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
*** empty log message ***
barras
2003-03-12
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Déplacement/renommage de Class.stre_max en Declare.strength_min
herbelin
2002-04-16
*
compat ocaml 3.03
filliatr
2001-12-13
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Code mort
herbelin
2001-11-20
*
Nettoyage coercions et classes
herbelin
2001-11-09
*
GROS COMMIT:
barras
2001-11-05
[next]