aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2004-04-13Correction confusion entre la dependance en les termes filtrees dans l'annota...herbelin
2004-04-07bug #606: mis un message d'erreur plus clairbarras
2004-04-05Déclaration des record au chargement (ce n'est pas une question de visibilit...herbelin
2004-03-29Typoherbelin
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...herbelin
2004-03-24bug de PP des fix (coqbugs #574)barras
2004-03-15preparation pour release (suite)barras
2004-03-09bug affichage des cofixbarras
2004-03-08correction de bugs des points fixesbarras
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-27Erreur de Bruijn et oubli substitution alias dans annotation du 'match'herbelin
2004-02-26Inclusion des annotations de type des filtrages dans 'Set Printing All'herbelin
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-02-13Deplacement array_map_left and co dans Utilherbelin
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (suite)herbelin
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...herbelin
2004-02-05On s'affranchit de l'information inductif ou pas dans le prédicat (càdherbelin
2004-02-05Suppression des types dans la signature du predicat (ils sontherbelin
2004-02-04Reconnaissance précoce de la dépendance du prédicat en un terme filtréherbelin
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...herbelin
2004-02-03Relachement condition pour declarer un inductif dans la table des 'If'; contr...herbelin
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ...herbelin
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...herbelin
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant que...herbelin
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...herbelin
2004-01-12Set is not always impredicativebarras
2003-12-27Type le 'return' comme un typeherbelin
2003-12-23Affichage opaqueherbelin
2003-12-19Substitution dans REvar; reparation bug 277herbelin
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application po...herbelin
2003-12-17Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'herbelin
2003-12-16Correction bug 371 (sub_match retournait des instances non closes)herbelin
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-21Ajout 'Simpl f'herbelin
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
2003-11-18Ajout mis_constructor_nargs_envherbelin
2003-11-09Ajout reduce_to_quantified_refherbelin
2003-11-04Amelioration message d'erreur pour ltacherbelin
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
2003-10-13Export is_section_variableherbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-13Deplacement de Declare vers Termopsherbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-12open superfluherbelin
2003-09-10Bug predicat old Caseherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 13:15:48 +0000