aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2009-01-14Fixing #1960 (xml bug with external on goal variable) and #1961herbelin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-11-27fixed non-exhaustive pattern matchingbarras
2008-08-04Évolutions diverses et variées.herbelin
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-21Addded the "Dump Tree" command.cek
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
2007-01-22Correction du bug #1315:notin
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