index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
record.ml
Commit message (
Expand
)
Author
Age
*
bugs avec Pose et Assert
barras
2004-01-09
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)
herbelin
2003-09-16
*
Mise en place possibilité de définitions locales dans les paramètres des r...
herbelin
2003-09-06
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Utilisation des de Bruijn pour la constructions des records et de leur projec...
herbelin
2002-05-13
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Amélioration messages d'erreur arité incorrecte (notamment record)
herbelin
2001-11-21
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Parsing
herbelin
2001-08-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
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Ajout de constantes locales dans les Records
herbelin
2001-01-24
*
correction de bugs sur commit précédent
herbelin
2000-12-19
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
uniformisation messages d'erreur
filliatr
2000-11-27
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
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
*
Messages d'erreurs
herbelin
2000-09-15
*
Abstraction de constr
herbelin
2000-09-14
*
Correction pour make doc
herbelin
2000-09-10
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
herbelin
2000-09-06
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Nettoyage de Generic
herbelin
2000-05-31
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...
herbelin
2000-03-28
*
Prise en compte nouveau case_info dans type_case
herbelin
2000-03-21
*
Ajout de Record
herbelin
2000-01-11
*
- global_reference traite des variables
filliatr
1999-12-03
*
Version initiale
herbelin
1999-12-02