aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Message d'erreur bad patternGravatar herbelin2000-10-11
* Messages d'erreurs CasesGravatar herbelin2000-10-10
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* renommage map_constr_with_named_bindersGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Code mortGravatar herbelin2000-10-01
* Messages d'erreursGravatar herbelin2000-09-15
* Expression anglaiseGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Fail n + appel de interpGravatar delahaye2000-07-21
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Bug: on tentait de déclarer un schéma d'induction pour un coinductifGravatar herbelin2000-07-01
* Essai de simplification compte tenu de l'info de locationGravatar herbelin2000-06-29
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* Bugs/Messages d'erreursGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Petit bug get_current_contextGravatar herbelin2000-05-25
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* export get_current_contextGravatar herbelin2000-05-18
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Retrait de PrintConstr vers top_printersGravatar delahaye2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* discharge des axiomesGravatar filliatr2000-04-21
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Portage (pour la forme) de minicoqGravatar herbelin2000-03-31
* Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...Gravatar herbelin2000-03-28
* Déplacement des fonctions spécifiques du discharge qui était dans Generic;...Gravatar herbelin2000-03-21
* Prise en compte nouveau case_info dans type_caseGravatar herbelin2000-03-21
* bug discharge (work_alist contenanti plein de fois les memes choses)Gravatar filliatr2000-03-18
* Réparation du cast oublié lors d'une définition castéeGravatar herbelin2000-03-08
* Force le renommage dans bad_ind_argumentsGravatar herbelin2000-01-31