aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
2002-05-21Field + MapleModedelahaye
2002-05-16MAJherbelin
2002-05-16ARCH passe de Makefile à config.distribherbelin
2002-05-16MAJherbelin
2002-05-16MAJ V7.3herbelin
2002-05-16Ajout Peano_dec et Compare_decherbelin
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
2002-05-15MAJherbelin
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
2002-05-15Contournement de la fermeture ML dans VContextherbelin
2002-05-15MAJherbelin
2002-05-15MAJ V7.3herbelin
2002-05-15majfilliatr
2002-05-15mention -dump-globfilliatr
2002-05-14MAJherbelin
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
2002-05-14petite erreur de syntaxebarras
2002-05-14modification de clenv_merge:barras
2002-05-14Ajout de la modification des sortes d'eliminationmohring
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
2002-05-14Changement de eq en eqT comme equivalence de setoide par defaut.clrenard
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
2002-05-13Utilisation des de Bruijn pour la constructions des records et de leur projec...herbelin
2002-05-13Pas de projection si le nom d'un champ est '_' dans un Recordherbelin
2002-05-10Plus de souplesse pour les constructeurs encapsulés sous des définitionsherbelin
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-06Cosmétiqueherbelin
2002-05-06Standardisationherbelin
2002-05-06MAJherbelin
2002-05-03Simplification du filtrage si la premiere ligne de motifs est inevitable + au...herbelin
2002-05-02Minor correction of get_lem_namecoq
2002-05-02nettoyage codecourant
2002-04-24petit bug dans les noms de fichiersletouzey
2002-04-19lemmes sur Zdiv/Zmodfilliatr
2002-04-19jLogic disparaîtherbelin
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...filliatr
2002-04-18Suppression d'un warning plus surprenant qu'utileherbelin
2002-04-18*** empty log message ***letouzey
2002-04-17*** empty log message ***werner
2002-04-17Ajout remarques diverses et tactiquesherbelin
2002-04-17typed unification in the case of Patternbarras
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-17jLogic.mli remplace par jolic.mliherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 09:49:06 +0000