aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-27MAJherbelin
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
2003-10-27Bug du commit precedentherbelin
2003-10-23majfilliatr
2003-10-23Saut de ligne avant les infos non logiques de print_aboutherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-23Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionherbelin
2003-10-23Independance de grammar.cmo vis a vis de Searchherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-23Commentairesherbelin
2003-10-23Jprover bugfix (hopefully !)corbinea
2003-10-22majfilliatr
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
2003-10-22MAJherbelin
2003-10-22Ajout NArithRingherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22MAJherbelin
2003-10-22Suppression dependance formelle en Vernacexprherbelin
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
2003-10-22Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de Se...herbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-22nouvelles priorites + Hintsbarras
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...herbelin
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
2003-10-21Redondance de dec_eq_natherbelin
2003-10-21Type relation dans Datatypesherbelin
2003-10-21Construction des chemins de constantes plus robusteherbelin
2003-10-21Optimisation de gen_constant_in_modulesherbelin
2003-10-21Extension de Locateherbelin
2003-10-21Nouvelle fonction cherchant tous les noms d'un suffixe donneherbelin
2003-10-21Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...herbelin
2003-10-21*** empty log message ***barras
2003-10-21Bug Locate Notationherbelin
2003-10-21Correction bug FreshIdherbelin
2003-10-21MAJherbelin
2003-10-21Maintenant avant Datatypesherbelin
2003-10-21ajoutsherbelin
2003-10-20majfilliatr
2003-10-20Globalisation des hints autorewriteherbelin
2003-10-20R passe dans Set !herbelin
2003-10-20bug traduction de auto.(simpl). en auto.simpl.barras
2003-10-20*** empty log message ***barras
2003-10-19Extension de l'utilisation de contradictionherbelin
2003-10-18Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteherbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-17majfilliatr
2003-10-17On n'autorise plus les niveaux doubles L/R en v8herbelin
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-07 16:09:41 +0000