aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
* Noms "canoniques" pour certaines des propriétés de xor.Gravatar herbelin2006-10-17
* Mise en forme des theoriesGravatar notin2006-10-17
* affichage des ... dans les scriptsGravatar barras2006-10-16
* typo doc + bug legacy fieldGravatar barras2006-10-16
* changes the use of lists and notations, to avoid that the notationsGravatar bertot2006-10-16
* Simplification ocamldebug (coq-debug-programs.out obsolète)Gravatar herbelin2006-10-13
* Ajout des options Coqide suggérées par Damien Doligez (wish #1053)Gravatar notin2006-10-13
* Adaptation des tests suite à la modification de Rewrite .. in (r9201)Gravatar notin2006-10-13
* Correction test-suite suite à r9186Gravatar notin2006-10-13
* Ajout du théorème mult_minus_distr_lGravatar notin2006-10-13
* r9778@tannat: jforest | 2006-10-13 11:36:37 +0200Gravatar jforest2006-10-13
* Protection raise en début de séquence (en attendant que le code caché trou...Gravatar herbelin2006-10-12
* Fix name clash on leftGravatar thery2006-10-12
* Ajout de pages de man pour les exécutables coqGravatar notin2006-10-11
* Ajout d'une option -annotate au configure+ changement du comportement par dé...Gravatar notin2006-10-11
* Fix 0 obligations bugGravatar msozeau2006-10-10
* Remove duplicate conditions in Field + Monomial substitution function for PExprGravatar thery2006-10-10
* make sure BinList is not made visible to files that use the tactic RingGravatar bertot2006-10-10
* Exemple avec liaison des variables de filtrage du matchGravatar herbelin2006-10-09
* Amélioration de l'automatisation des coupures quand deux idents se suiventGravatar herbelin2006-10-09
* Notations:Gravatar herbelin2006-10-09
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
* suite commit 9222 : rétablissement des tests autre que complexitéGravatar herbelin2006-10-06
* Remplacement des nf_evar (source de complexité polynomiale) par de laGravatar herbelin2006-10-06
* Ajout d'un répertoire de test de la complexitéGravatar herbelin2006-10-06
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* Suppression d'une source de complexité polynomiale dans le pretypageGravatar herbelin2006-10-06
* MAJGravatar herbelin2006-10-06
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
* Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...Gravatar notin2006-10-05
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* revert, the previous commit was a mistakeGravatar bertot2006-10-05
* avertissement a propos du commit 9211 dans CHANGESGravatar letouzey2006-10-05
* A version of natprering that should be more efficient and removal of a badGravatar bertot2006-10-05
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
* Corrects the problem described in PR#1240:Gravatar bertot2006-10-05
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
* Ajout StringGravatar herbelin2006-10-04
* inefficacite de field_simplify_eqGravatar barras2006-10-04
* Correction bug #1211Gravatar notin2006-10-04
* Correction bug #1204 + maj CHANGESGravatar notin2006-10-04
* Correction bug #1236Gravatar notin2006-10-04
* Doc injection asGravatar herbelin2006-10-04
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* le parsing du LETIN ne suivait pas la DTD (bug #1237)Gravatar herbelin2006-10-03
* Retour sur la suppression du pf_nf (trop d'exemples utilisent avecGravatar herbelin2006-10-03
* Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...Gravatar herbelin2006-10-03
* nouveau ring/fieldGravatar barras2006-10-02