aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2000-05-05docherbelin
2000-05-05Ajout d'un strong 'light'herbelin
2000-05-05ajout interp_sortherbelin
2000-05-05Réorganisationherbelin
2000-05-05Achèvement nettoyage Pfedit; ajout intros_replacingherbelin
2000-05-05Intégration de leminvherbelin
2000-05-05Achèvement nettoyage Pfeditherbelin
2000-05-05Ajoute option -byteherbelin
2000-05-04MAJherbelin
2000-05-04Vernacinterp passe après Commandherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:52:40 +0000