aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
AgeCommit message (Expand)Author
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
2004-04-05Since coqdoc produces (X)HTML, HTML character entities can be usedsacerdot
2004-04-04** WARNING **sacerdot
2004-04-01LocalFact added as a choice for the "as" attribute of ht:VARIABLE in thesacerdot
2004-04-01Big bug fixed: interactive local definitions where handled as constantssacerdot
2004-04-01Output of theory files reimplemented using Buffer.sacerdot
2004-04-01~keep_sections was now redundant. Got rid of.sacerdot
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ...herbelin
2004-03-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
2004-03-30*** WARNING: DTD Change ***sacerdot
2004-03-30declare_internal_constant behaved as declare_constant for proofs (e.g.sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 12:41:12 +0000