aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-06-02bugs infrence des arguments manquants dans le prdicatherbelin
2000-06-02bugs et simplification (suite)herbelin
2000-06-02docherbelin
2000-06-02MAJherbelin
2000-06-02Bug DLAM dans strongherbelin
2000-06-02Bugs/Messages d'erreursherbelin
2000-06-02Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-06-02Bugs et simplifications coercionsherbelin
2000-06-02':>' est devenu un seul tokenherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Afficahge des locationsherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-31docherbelin
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
2000-05-31Amélioration capture des erreursherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
2000-05-25Petit bug get_current_contextherbelin
2000-05-23Bug de castherbelin
2000-05-23Bug stupide d'ordre d'évaluationherbelin
2000-05-23Réparation bug d'affichage et affichage des instanciations par des {...}herbelin
2000-05-23MAJherbelin
2000-05-23Docherbelin
2000-05-22Commentairesherbelin
2000-05-22Séparation des tokens -> et ~herbelin
2000-05-22Rienherbelin
2000-05-22Bugs d'index d'inductiveherbelin
2000-05-22Renommage hypothèses de nom redondant dans les environnementsherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Fichiers des modifs pour l'utilisateursherbelin
2000-05-22Changement nommage des hypothèses; parenthèses pour les tactiquesherbelin
2000-05-22Changement nommage des hypothèsesherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-22Changement nom module Constant en Declarationsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-22Parenthèsesherbelin
2000-05-22Retour comportement de la version précédenteherbelin
2000-05-18bug (typage avec meta)herbelin
2000-05-18parethèses de tactiquesherbelin
2000-05-18bugsherbelin
2000-05-18suppression ligne etrangeherbelin
2000-05-18export get_current_contextherbelin
2000-05-18Ajout warning si variable existant par ailleursherbelin
2000-05-18ciseauxherbelin
2000-05-18MAJ modifs Inductiveherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-18Ajouts des causes d'erreur de Indrecherbelin
2000-05-18MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 20:19:19 +0000