aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
AgeCommit message (Expand)Author
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-16affichage des ... dans les scriptsbarras
2006-10-03Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...herbelin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-07-18Correction bug #1192notin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-05-23Clarification role de library_part : renommage en remove_section_partherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-27Message d'erreur plus informatifherbelin
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-02Types inductifs parametriquesmohring
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-03-15Unsharing before exportation to ensure uniqueness of xml id'sherbelin
2005-02-18Standardisation of function names about structuresherbelin
2005-02-04Ajout printer direct cic vers xmlherbelin
2005-02-04Export du printer xml vers tacinterpherbelin
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-12-03Orthographe!herbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-08The innersort is now computed as the more precise sort between thesacerdot
2004-09-08The code used to compare the synthesized and the expected type (if available)sacerdot
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2004-07-08* <style>...</style> tag no longer generated for theory filessacerdot
2004-07-08- recent changes to doubleTypeInference.ml (that introduced doublesacerdot
2004-07-08Commit to perform double type inference also on inner types.sacerdot
2004-07-05Constants just after a "Let id : t. ... Qed" local variable declaration weresacerdot
2004-06-30updated printing of evar context (may loop ?)corbinea
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
2004-04-07Old file. The new version of this script is no longer distributed withsacerdot
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
2004-04-07CoRN CProp detection improved: products of "sort" CProp are now recognizedsacerdot
2004-04-07Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;sacerdot
2004-04-06Fake dependent products in inductive definition types are no longer replacedsacerdot
2004-04-06Important bug fix: since coqdoc is now quoting XML reserved characters insacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 06:09:23 +0000