index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
declarations.ml
Commit message (
Expand
)
Author
Age
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
- Correction bug calcul mind_consnrealargs, introduit à la révision
herbelin
2006-03-22
*
Documentation mutual_inductive_body
herbelin
2006-03-18
*
Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...
herbelin
2006-01-10
*
Changement des named_context
gregoire
2005-12-02
*
Types inductifs parametriques
mohring
2005-11-02
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Ajout recarg_length
herbelin
2003-11-18
*
coupage en deux du bloc pas si mutuellement recursif des module_body & co (.....
letouzey
2003-04-16
*
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-12-09
*
suppression du champ mind_singl inutilisé dans mutual_inductive_body
letouzey
2002-12-04
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
entetes
filliatr
2001-03-15
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Ajout mind_arities_env
herbelin
2000-10-11
*
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Précalcul de la forme canonique des constructeurs et arités pour traiter le...
herbelin
2000-07-01
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs
herbelin
2000-05-31
*
Changement nom module Constant en Declarations
herbelin
2000-05-22