index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
indtypes.ml
Commit message (
Expand
)
Author
Age
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Inductive Types : seuls les petits types sont unitaires
mohring
2003-12-19
*
modif lexer: ident peut commencer par _
barras
2003-11-25
*
Suppression StronglyClassical, StronglyConstructive devient plus concretement...
herbelin
2003-11-08
*
Message inductive large
herbelin
2003-10-28
*
Set devient predicatif par defaut
herbelin
2003-10-28
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
suppression du champ mind_singl inutilisé dans mutual_inductive_body
letouzey
2002-12-04
*
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
*
erreur mineure dans le test des inductifs imbriques
barras
2002-02-07
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
Reparation erreur de syntaxe
mohring
2002-01-30
*
modification de la definition des def inductives unitaires et autorisation d'...
mohring
2002-01-29
*
condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...
barras
2002-01-29
*
Cas LetIn superflu dans check_construct car normalisation préalable
herbelin
2002-01-24
*
correction de bug avec les mutuels imbriques a plusieurs niveaux
barras
2002-01-16
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
corrections mineures suite au commit de restructuration du noyau
barras
2001-11-06
*
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
*
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
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
entetes
filliatr
2001-03-15
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
- suppression mind_extract_params
filliatr
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-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
*
Prise en compte de l'environnement dans les tests de correction des inductifs
herbelin
2000-10-11
*
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
*
On laisse les LetIn dans les types des constructeurs et des éliminations
herbelin
2000-09-15
*
Abstraction de constr
herbelin
2000-09-14
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
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
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Ajouts des causes d'erreur de Indrec
herbelin
2000-05-18
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
Prise en compte nouveau case_info
herbelin
2000-03-21
*
Nettoyage check_pos
herbelin
2000-03-07
[next]