aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* suite du commit precedentGravatar barras2002-12-19
* pretyping/pretyping.mlGravatar herbelin2002-09-03
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* Un ++ au lieu d'un ;Gravatar herbelin2001-12-21
* Nettoyage exceptions liées au vieux CaseGravatar herbelin2001-12-18
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* Amélioration message CasesGravatar herbelin2001-11-21
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* OrthographeGravatar herbelin2001-10-15
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Pretty -> PrettypGravatar filliatr2001-05-28
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* Amelioration message args constructeurGravatar herbelin2001-04-25
* Messages d'erreur CasesGravatar herbelin2001-04-24
* Mise en place d'un test de clauses non utiliseesGravatar herbelin2001-04-13
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Typo message SchemeGravatar herbelin2001-02-28
* Amélioration message d'erreur mauvais prédicatGravatar herbelin2000-12-18
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
* Ajout erreur DoesNotOccurInGravatar herbelin2000-12-06
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
* uniformisation messages d'erreurGravatar filliatr2000-11-27
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
* améliorationGravatar herbelin2000-11-08
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Message d'erreur bad patternGravatar herbelin2000-10-11
* Messages d'erreurs CasesGravatar herbelin2000-10-10
* Expression anglaiseGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* kernel/type_errors.mlGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Essai de simplification compte tenu de l'info de locationGravatar herbelin2000-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 10:39:25 +0000