aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Fichiers des modifs pour l'utilisateursGravatar herbelin2000-05-22
* Changement nommage des hypothèses; parenthèses pour les tactiquesGravatar herbelin2000-05-22
* Changement nommage des hypothèsesGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* ParenthèsesGravatar herbelin2000-05-22
* Retour comportement de la version précédenteGravatar herbelin2000-05-22
* bug (typage avec meta)Gravatar herbelin2000-05-18
* parethèses de tactiquesGravatar herbelin2000-05-18
* bugsGravatar herbelin2000-05-18
* suppression ligne etrangeGravatar herbelin2000-05-18
* export get_current_contextGravatar herbelin2000-05-18
* Ajout warning si variable existant par ailleursGravatar herbelin2000-05-18
* ciseauxGravatar herbelin2000-05-18
* MAJ modifs InductiveGravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajouts des causes d'erreur de IndrecGravatar herbelin2000-05-18
* MAJGravatar herbelin2000-05-18
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Ajout lift_contextGravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* Adaptation pour nouveaux inductifs (cf Inductive)Gravatar herbelin2000-05-18
* NettoyageGravatar herbelin2000-05-18
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* docGravatar herbelin2000-05-18
* Ajout mis_typepathGravatar herbelin2000-05-16
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* RIENGravatar herbelin2000-05-16
* RienGravatar herbelin2000-05-16
* contrib linkees en natifGravatar filliatr2000-05-08
* un Declare ML Module inutileGravatar filliatr2000-05-08
* ajout d'InversionGravatar filliatr2000-05-05
* MAJGravatar herbelin2000-05-05
* docGravatar herbelin2000-05-05
* Ajout d'un strong 'light'Gravatar herbelin2000-05-05
* ajout interp_sortGravatar herbelin2000-05-05
* RéorganisationGravatar herbelin2000-05-05
* Achèvement nettoyage Pfedit; ajout intros_replacingGravatar herbelin2000-05-05
* Intégration de leminvGravatar herbelin2000-05-05
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
* Ajoute option -byteGravatar herbelin2000-05-05
* MAJGravatar herbelin2000-05-04
* Vernacinterp passe après CommandGravatar herbelin2000-05-04
* les erreursGravatar herbelin2000-05-04
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04