aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-10-17Clarification des contraintes sur le contexte de paramètres desherbelin
2006-10-17Noms "canoniques" pour certaines des propriétés de xor.herbelin
2006-10-17Mise en forme des theoriesnotin
2006-10-16affichage des ... dans les scriptsbarras
2006-10-16typo doc + bug legacy fieldbarras
2006-10-16changes the use of lists and notations, to avoid that the notationsbertot
2006-10-13Simplification ocamldebug (coq-debug-programs.out obsolète)herbelin
2006-10-13Ajout des options Coqide suggérées par Damien Doligez (wish #1053)notin
2006-10-13Adaptation des tests suite à la modification de Rewrite .. in (r9201)notin
2006-10-13Correction test-suite suite à r9186notin
2006-10-13Ajout du théorème mult_minus_distr_lnotin
2006-10-13 r9778@tannat: jforest | 2006-10-13 11:36:37 +0200jforest
2006-10-12Protection raise en début de séquence (en attendant que le code caché trou...herbelin
2006-10-12Fix name clash on leftthery
2006-10-11Ajout de pages de man pour les exécutables coqnotin
2006-10-11Ajout d'une option -annotate au configure+ changement du comportement par dé...notin
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