aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-12-19reparation du make depend et du .dependletouzey
2001-12-19MAJherbelin
2001-12-19Corrections post contournement des streams avec ++herbelin
2001-12-19Réorganisationherbelin
2001-12-19Pour les développeurs extérieursherbelin
2001-12-19MAJ V7.2herbelin
2001-12-19MAJherbelin
2001-12-19MAJherbelin
2001-12-19NatRing (2ème)herbelin
2001-12-19NatRingherbelin
2001-12-19Le cas LetIn avait été oublié dans case_branches_specifherbelin
2001-12-19Un peu plus d'inférence des ? traitée par le Casesherbelin
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ...herbelin
2001-12-19reparation de make doc (ocamlweb & _)letouzey
2001-12-18the function Ctast.section_path was wrong. It performed two reversebertot
2001-12-18Pour ocamlweb ...letouzey
2001-12-18Oubli d'un quoteherbelin
2001-12-18On ne peut plus appliquer des arguments à une syntaxe primitiveherbelin
2001-12-18There remained traces of streams with the old syntax.bertot
2001-12-18Add a new file in the files needed for the "coq-interface" binary: the filebertot
2001-12-18Add dependencies for two new files in contrib/interfacebertot
2001-12-18Integrating the Ltac language and the Blast tool into the interfacebertot
2001-12-18affichage correct du type des inductifs et constructeurs en presencebarras
2001-12-18typo de parenthèsage + suppression de string (= str maintenant)letouzey
2001-12-18anti revolution culturelle: retour des arguments logiquesletouzey
2001-12-18ote les redondances des entetesletouzey
2001-12-18coq-bugs #12: probleme de metamap resolubarras
2001-12-18MAJherbelin
2001-12-18parsing des branches de Cases au niveau lconstr (au lieu de constr)barras
2001-12-18Grossière erreur de typageherbelin
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
2001-12-18Nettoyage exceptions liées au vieux Case; réparation du try with UserError ...herbelin
2001-12-17Mauvais nom d'erreur d'échec de nthherbelin
2001-12-17probleme des Require dans les sectionsbarras
2001-12-17le save de Correctness faisant assert falsebarras
2001-12-16Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...herbelin
2001-12-13MAJherbelin
2001-12-13*** empty log message ***herbelin
2001-12-13MAJ de la traduction en ast des variables de section en qualidherbelin
2001-12-13Contournement du problème des evars de type, typées par défaut dans Type (...herbelin
2001-12-13Affichage NewInduction/NewDesctructherbelin
2001-12-13Contournement du problème des evars de type, typées par défaut dans Typeherbelin
2001-12-13package Debian 7.1, correction pb compilation native sur certaines architecturescourant
2001-12-13compat ocaml 3.03filliatr
2001-12-12MAJherbelin
2001-12-11suppression de l'affichage des noeuds Change_evarsbarras
2001-12-11*** empty log message ***courant
2001-12-11ajout du document sur la nouvelle syntaxebarras
2001-12-11document sur les propositions de nouvelle syntaxebarras
2001-12-11Mise en place de coercion dans les motifsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-21 19:36:17 +0000