aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-10-10Fix 0 obligations bugmsozeau
2006-10-10Remove duplicate conditions in Field + Monomial substitution function for PExprthery
2006-10-10make sure BinList is not made visible to files that use the tactic Ringbertot
2006-10-09Exemple avec liaison des variables de filtrage du matchherbelin
2006-10-09Amélioration de l'automatisation des coupures quand deux idents se suiventherbelin
2006-10-09Notations:herbelin
2006-10-09Ajout combinateurs option_fold_left et name_fold_mapherbelin
2006-10-06suite commit 9222 : rétablissement des tests autre que complexitéherbelin
2006-10-06Remplacement des nf_evar (source de complexité polynomiale) par de laherbelin
2006-10-06Ajout d'un répertoire de test de la complexitéherbelin
2006-10-06Déplacement de on_judgment_type de Typeops vers Termopsherbelin
2006-10-06Suppression d'une source de complexité polynomiale dans le pretypageherbelin
2006-10-06MAJherbelin
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
2006-10-05Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...notin
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-10-05revert, the previous commit was a mistakebertot
2006-10-05avertissement a propos du commit 9211 dans CHANGESletouzey
2006-10-05A version of natprering that should be more efficient and removal of a badbertot
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
2006-10-05Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynombarras
2006-10-05Corrects the problem described in PR#1240:bertot
2006-10-05Essai de changement de sémantique du %scope : herbelin
2006-10-04Ajout Stringherbelin
2006-10-04inefficacite de field_simplify_eqbarras
2006-10-04Correction bug #1211notin
2006-10-04Correction bug #1204 + maj CHANGESnotin
2006-10-04Correction bug #1236notin
2006-10-04Doc injection asherbelin
2006-10-03Changement de comportement du [rewrite ... in H]: Coq échoue si Hnotin
2006-10-03le parsing du LETIN ne suivait pas la DTD (bug #1237)herbelin
2006-10-03Retour sur la suppression du pf_nf (trop d'exemples utilisent avecherbelin
2006-10-03Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...herbelin
2006-10-02nouveau ring/fieldbarras
2006-10-02bug dans field_simplifybarras
2006-10-01Une passe sur l'injection et la discrimination...herbelin
2006-10-01Ajout allowed_sortsherbelin
2006-09-30Suppression de la comparaison (inutile) des paramètres globaux desherbelin
2006-09-29args implicites dans Fieldbarras
2006-09-29Added a new option -emacs-U changing emacs prompt delimiters bycourtieu
2006-09-29Reactivation des outils de developpement de Jacekherbelin
2006-09-29Suppression des warnings à la compilationnotin
2006-09-29git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...barras
2006-09-28separation de RealFieldbarras
2006-09-28Suppression des lignes vides dans l'affichage des scriptsnotin
2006-09-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...barras
2006-09-28Add dependent list combinators test.msozeau
2006-09-28Makefile : COQLIB -> FULLCOQLIBcorbinea
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
2006-09-26petits pbs de dependancesbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 21:38:11 +0000