aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml
Commit message (Expand)AuthorAge
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Addded the "Dump Tree" command.Gravatar cek2008-04-21
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Correction de plusieurs bugs de l'export XML (utilisation d'un type deGravatar herbelin2007-06-21
* Correction du bug #1315:Gravatar notin2007-01-22
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* affichage des ... dans les scriptsGravatar barras2006-10-16
* Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...Gravatar herbelin2006-10-03
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Correction bug #1192Gravatar notin2006-07-18
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Message d'erreur plus informatifGravatar herbelin2006-04-27
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Unsharing before exportation to ensure uniqueness of xml id'sGravatar herbelin2005-03-15
* Standardisation of function names about structuresGravatar herbelin2005-02-18
* Ajout printer direct cic vers xmlGravatar herbelin2005-02-04
* Export du printer xml vers tacinterpGravatar herbelin2005-02-04
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* Orthographe!Gravatar herbelin2004-12-03
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* The innersort is now computed as the more precise sort between theGravatar sacerdot2004-09-08
* The code used to compare the synthesized and the expected type (if available)Gravatar sacerdot2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* * <style>...</style> tag no longer generated for theory filesGravatar sacerdot2004-07-08
* - recent changes to doubleTypeInference.ml (that introduced doubleGravatar sacerdot2004-07-08
* Commit to perform double type inference also on inner types.Gravatar sacerdot2004-07-08