aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2006-09-26Compilation newringnotin
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-26fixed error mesg in decl modecorbinea
2006-09-25Corrections mineuresnotin
2006-09-25 Permet a un unfold de recevoir ses occurences a travers une variable Ltac.letouzey
2006-09-24Tentative d'amélioration du message d'erreur en cas de paramètre non laisséherbelin
2006-09-24Correction bug dans détection clause "in" mal formée quand le "in" estherbelin
2006-09-23Correction d'un bug de coercion de pattern introduit dans la 8.1betaherbelin
2006-09-23Correction bug #1168 (dans les coercions de pattern, c'est le nombreherbelin
2006-09-23Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderherbelin
2006-09-23Wish #1187 granted (support for canonical structures that are recordsherbelin
2006-09-23Correction bug #1229 (toplevel "unresolved evar" fled throughherbelin
2006-09-23Déplacement surround dans util.ml et parenthésage des déclarationsherbelin
2006-09-23- Correction filtrage des notations impliquant un "match" : la présenceherbelin
2006-09-22Protection List.fold_left2 (cf bug #1224)herbelin
2006-09-22Tout petit bug d'affichage dans constr_display (top_printers)herbelin
2006-09-22Test Tactic Notationherbelin
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
2006-09-22doc du nouveau ringbarras
2006-09-21Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...herbelin
2006-09-21incomplete and temporary fix for PR#1222: revert accepts up to 10 argsletouzey
2006-09-21better scope/require managment (patch by Russel O'Connor)letouzey
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-20congruence doc updatecorbinea
2006-09-19Gestion des arguments implicites dans les Functions bien fondeesjforest
2006-09-19added congruence improvementcorbinea
2006-09-18correction of bug #1220jforest
2006-09-18Correction du bug #1215notin
2006-09-16Message modification in Functionjforest
2006-09-15Compatibilité hyp=var dans Tactic Notation + nettoyageherbelin
2006-09-15Minor bug correction in well-founded Function.jforest
2006-09-15MAJherbelin
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
2006-09-15Débogage: ajout affichage contraintes d'unificationherbelin
2006-09-14Bug dans configure (test best_compiler)notin
2006-09-14Correction du bug #1181jforest
2006-09-14Compilation de Coq sous Windowsnotin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:15:46 +0000