index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
Essai de suppression de eta dans simpl (cf bug #779)
herbelin
2004-06-29
*
Double bug d'affichage des cases dépendants (bug #784)
herbelin
2004-06-28
*
Correction affichage v8 des records avec let (bug #798)
herbelin
2004-06-27
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
test de conversion laissait echapper exception NotConvertible
barras
2004-05-14
*
Terminologie plus intuitive: evaluable -> unfoldable
herbelin
2004-04-30
*
Prise en compte d'un type dont la sorte est une evar
herbelin
2004-04-29
*
Correction incapacité à gérer les annotations de type dépendantes pour le...
herbelin
2004-04-27
*
Correction confusion entre la dependance en les termes filtrees dans l'annota...
herbelin
2004-04-13
*
bug #606: mis un message d'erreur plus clair
barras
2004-04-07
*
Déclaration des record au chargement (ce n'est pas une question de visibilit...
herbelin
2004-04-05
*
Typo
herbelin
2004-03-29
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
bug de PP des fix (coqbugs #574)
barras
2004-03-24
*
preparation pour release (suite)
barras
2004-03-15
*
bug affichage des cofix
barras
2004-03-09
*
correction de bugs des points fixes
barras
2004-03-08
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Erreur de Bruijn et oubli substitution alias dans annotation du 'match'
herbelin
2004-02-27
*
Inclusion des annotations de type des filtrages dans 'Set Printing All'
herbelin
2004-02-26
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Deplacement array_map_left and co dans Util
herbelin
2004-02-13
*
Bug numerotation des occurrences pour 'simpl id at n' (suite)
herbelin
2004-02-13
*
Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...
herbelin
2004-02-13
*
On s'affranchit de l'information inductif ou pas dans le prédicat (cà d
herbelin
2004-02-05
*
Suppression des types dans la signature du predicat (ils sont
herbelin
2004-02-05
*
Reconnaissance précoce de la dépendance du prédicat en un terme filtré
herbelin
2004-02-04
*
Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...
herbelin
2004-02-04
*
Relachement condition pour declarer un inductif dans la table des 'If'; contr...
herbelin
2004-02-03
*
Backtrack sur recuperation de noms a partir du type, car casse la correction ...
herbelin
2004-02-03
*
Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...
herbelin
2004-01-29
*
Reparation d'une rupture (en presence de types implicites) de l'invariant que...
herbelin
2004-01-29
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
Set is not always impredicative
barras
2004-01-12
*
Type le 'return' comme un type
herbelin
2003-12-27
*
Affichage opaque
herbelin
2003-12-23
*
Substitution dans REvar; reparation bug 277
herbelin
2003-12-19
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'
herbelin
2003-12-17
*
Correction bug 371 (sub_match retournait des instances non closes)
herbelin
2003-12-16
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Ajout 'Simpl f'
herbelin
2003-11-21
*
Deplacement subst_rawconstr dans Rawterm
herbelin
2003-11-19
*
Ajout mis_constructor_nargs_env
herbelin
2003-11-18
*
Ajout reduce_to_quantified_ref
herbelin
2003-11-09
*
Amelioration message d'erreur pour ltac
herbelin
2003-11-04
*
Deplacement de iter_constr_with_full_binders dans Termops
herbelin
2003-10-22
*
Export is_section_variable
herbelin
2003-10-13
[next]