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