aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Ajout EVALherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Pour les tactiques dépendant de Falseherbelin
2002-05-29Implante la macro camlp4 VERNAC COMMAND EXTENDherbelin
2002-05-29Implante la macro camlp4 TACTIC EXTENDherbelin
2002-05-29Fichier des expressions de commandes vernaculairesherbelin
2002-05-29Fichier des expressions de tactiquesherbelin
2002-05-29MAJ 7.3herbelin
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-05-27Changement Filename.is_relative en Filename.is_implicit, plus pertinentherbelin
2002-05-22Oublisherbelin
2002-05-22*** empty log message ***desmettr
2002-05-22*** empty log message ***herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 10:05:34 +0000