aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-29*** empty log message ***herbelin
2003-10-29Choix sous sa forme relationnelleherbelin
2003-10-29majfilliatr
2003-10-28MAJherbelin
2003-10-28Ordre (symbolique) des Requireherbelin
2003-10-28Passage de la notations de paire dans core_scopeherbelin
2003-10-28Passage des notations de type dans type_scopeherbelin
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
2003-10-28Simplification preuveherbelin
2003-10-28Ajout de Print Visibilityherbelin
2003-10-28Ajout %core; MAJ niveau connecteurs logiqueherbelin
2003-10-28Affichage Assert_failure en ocaml 3.07herbelin
2003-10-28Message inductive largeherbelin
2003-10-28Nouveaux fichiers dans Logicherbelin
2003-10-28Nouveaux fichiers dans Logic; prise en compte de l'option -strongly-classical...herbelin
2003-10-28Options -strongly-constructive et -strongly-classicalherbelin
2003-10-28Set devient predicatif par defautherbelin
2003-10-28MAJherbelin
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
2003-10-28La logique sur Type inclut celle sur Setherbelin
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report 're...herbelin
2003-10-27Bug Double Inversionherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 02:31:28 +0000