aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
Commit message (Expand)AuthorAge
* 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
* Bugs/Messages d'erreursGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Force le renommage dans bad_ind_argumentsGravatar herbelin2000-01-31
* message erreur SchemeGravatar herbelin1999-12-15
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* Suppression Rel de rawconstr et correction de bugs d'affichageGravatar herbelin1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* premier debugageGravatar filliatr1999-12-05
* - coqmktopGravatar filliatr1999-12-03
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* On se fait la main: plus de precision si ill-formed rec bodyGravatar herbelin1999-11-10
* module LogicGravatar filliatr1999-10-14
* affichage des erreurs de typage dans minicoqGravatar filliatr1999-09-10
* module Himsg, comme un foncteurGravatar filliatr1999-09-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 21:12:50 +0000