index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
Chgt signature de type_of_existential
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...
herbelin
2001-01-31
*
make doc
herbelin
2001-01-27
*
Ajout alias mutual_inductive_path = section_path
herbelin
2001-01-27
*
Ajout global_vars_decl
herbelin
2001-01-24
*
Doc
herbelin
2001-01-24
*
Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...
herbelin
2000-12-26
*
Alias variable_path
herbelin
2000-12-25
*
Bug mauvais environnement dans le test d'eta-conversion
herbelin
2000-12-20
*
Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name
herbelin
2000-12-18
*
Le bon choix, c'est finalement identifier = string
herbelin
2000-12-15
*
Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...
herbelin
2000-12-15
*
- suppression mind_extract_params
filliatr
2000-12-15
*
Petite réorganisation
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
MAJ commentaires
herbelin
2000-12-14
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-12-06
*
Mini-nettoyage noms longs
herbelin
2000-12-05
*
Prise en compte de la contrainte de type dans Definition comme étant un cast...
herbelin
2000-11-29
*
Ajout d'un test pour vérifier qu'on a affaire à un ident
herbelin
2000-11-29
*
Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage
herbelin
2000-11-29
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Faut-il mettre la réduction let-in dans la réduction unfold ?
herbelin
2000-11-27
*
On déplie les locaux dans les types plutôt que de les quantifier par un Let
herbelin
2000-11-27
*
Utilisation de Let In pour les constantes locales, prise en compte des Let In...
herbelin
2000-11-27
*
Bug dans la gestion du contexte en présence de Fix dans le calcul de garde
herbelin
2000-11-27
*
Prise en compte des let in dans les instances de globaux
herbelin
2000-11-27
*
Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...
herbelin
2000-11-27
*
Ajout map_constr_with_full_binders et strong pour Simpl
herbelin
2000-11-27
*
Généralisation de constant_opt_value en reference_opt_value
herbelin
2000-11-27
*
Bug dans le calcul des dépendances dans add_discharged_constant
herbelin
2000-11-27
*
Prise en compte de noms absolus dans la nametab
herbelin
2000-11-26
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp
herbelin
2000-11-23
*
Ajout push_rels_assum
herbelin
2000-11-23
*
Reparation IsMutConstruct + Transparent
mohring
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
Reparation bug mutuels ind
mohring
2000-11-22
*
Ajout d'une fonction pour recuperer la liste des constantes
delahaye
2000-11-21
*
implicites manuels
filliatr
2000-11-21
*
Tables séparées pour chaque type de global
herbelin
2000-11-20
[next]