aboutsummaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
AgeCommit message (Expand)Author
2003-03-31Restauration de make_all_different (disparu depuis version 1.74) car sinon de...herbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-12*** empty log message ***barras
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-19suite du commit precedentbarras
2002-09-03pretyping/pretyping.mlherbelin
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
2001-12-21Un ++ au lieu d'un ;herbelin
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-21Amélioration message Casesherbelin
2001-11-21Amélioration messages d'erreur arité incorrecte (notamment record)herbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-15Orthographeherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-05-28Pretty -> Prettypfilliatr
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-03Changement de la structure des points fixesbarras
2001-04-25Amelioration message args constructeurherbelin
2001-04-24Messages d'erreur Casesherbelin
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-28Typo message Schemeherbelin
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
2000-12-14Raffinement erreur Wrong Predicateherbelin
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
2000-11-27uniformisation messages d'erreurfilliatr
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-20Ajout erreur GlobalNotFoundherbelin
2000-11-08améliorationherbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Renommage canonique :herbelin
2000-10-11Message d'erreur bad patternherbelin
2000-10-10Messages d'erreurs Casesherbelin
2000-09-15Expression anglaiseherbelin
2000-09-14Abstraction de constrherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-06kernel/type_errors.mlherbelin