aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-18Ajout lift_contextherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
2000-05-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
2000-05-18Nettoyageherbelin
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
2000-05-18docherbelin
2000-05-16Ajout mis_typepathherbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-16RIENherbelin
2000-05-16Rienherbelin
2000-05-08contrib linkees en natiffilliatr
2000-05-08un Declare ML Module inutilefilliatr
2000-05-05ajout d'Inversionfilliatr
2000-05-05MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 07:08:03 +0000