aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-04-03transformation des evar en meta preserve la linearite des metasbarras
2002-04-03changement de l'undo limitbarras
2002-04-02Optimisationdesmettr
2002-04-02Suppression PI_lb et PI_ubdesmettr
2002-04-02Suppression Fielddesmettr
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-03-29sans utiliser Fielddesmettr
2002-03-29Correction bug infix sur des varaiablesmohring
2002-03-29*** empty log message ***mohring
2002-03-29Suppression des invocations a Fielddesmettr
2002-03-28reparation du cas des arguments de type qui sont des arités + patch dummy ap...letouzey
2002-03-28petite erreur dans le typage des let-inbarras
2002-03-27Bug d'affichage des erreurs localisées dans un fichier suite àherbelin
2002-03-27Simplification de Proof_type.prim_ruleherbelin
2002-03-27Elimination Elimdep.vmohring
2002-03-27*** empty log message ***mohring
2002-03-26Refonte complete de la génération des types MLletouzey
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-03-22*** empty log message ***werner
2002-03-22code redondantherbelin
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-03-22An intuitionistic first-order theorem prover -- JProver.huang
2002-03-21backtrack de l'unificationbarras
2002-03-21reparation du test des realsletouzey
2002-03-21Décomposition de l'application n-aire en application binaire pour que Patter...herbelin
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
2002-03-21considerations de pretty-printletouzey
2002-03-21deux fichiers supplementaires de customisation d'extractionletouzey
2002-03-21changement du test extraction suite aux modif ininingletouzey
2002-03-21modification de l'auto-inliningletouzey
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
2002-03-20encore quelques petites modif de l'unificationbarras
2002-03-20renversement du renommage des variablesletouzey
2002-03-20reparation du controle de l'apparition des termesletouzey
2002-03-20reorganisation des simplifications: letin eta-expansé apres le kill-dummyletouzey
2002-03-20un peu moins d'eta-expansion autour des Globletouzey
2002-03-19bug optimize_fix fait trop totletouzey
2002-03-19suite bug Dglob constantletouzey
2002-03-19bug avec les MLglob vraiment constantsletouzey
2002-03-19travail sur les stratégies de réductionletouzey
2002-03-19remplacement des deux constants prop/arity par une seule dummy + pretty-print...letouzey
2002-03-19Ajout de l'entrée ne_constrarg_listdelahaye
2002-03-19Fix d'un bug sur le test des inversesdelahaye
2002-03-19Exportation de SplitRmult et SplitAbsoludelahaye
2002-03-18Rétablissement de look_for_interpdelahaye
2002-03-17Field ne fait maintenant que les reductions necessairesdelahaye
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
2002-03-15epsilonletouzey
2002-03-15changements récents dans l'extractionletouzey
2002-03-15un peu de mise a jour de la doc extractionletouzey