aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-03-17MAJ test complexité pour considérer le cas d'un temps avec un nombreherbelin
2007-03-16Correction du bug #1441notin
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
2007-03-15Test de non-régression pour commit 9673herbelin
2007-03-15Typosherbelin
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
2007-03-15Add destruct_call variant where naming of introduced hypotheses is possible. ...msozeau
2007-03-14Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...msozeau
2007-03-14Bug dans Makefile (COQINSTALLPREFIX)notin
2007-03-14Removed an unnecessary argument (p : positive) in Prect_base.emakarov
2007-03-13Solve obligation handling bug of trying to solve automatically at Next Obliga...msozeau
2007-03-13Correction bug #1439 (comportement de replace by)notin
2007-03-12Proof simplification for eq_nat_dec et le_lt_dec: induction over letouzey
2007-03-11correction du bug 1432jforest
2007-03-11Remove bugguy notationsmsozeau
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
2007-03-08Create a program_scope in subtac Utilsmsozeau
2007-03-08Add Program keywords to coqwcmsozeau
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
2007-03-07Application suggestion #1430 de Yevgeniy pour TEXINPUTSherbelin
2007-03-06màj dépendances .v: SubtacTactics.volmamane
2007-02-28FSetInterface: new item choose_equal in the spec S (request of P. Casteran)letouzey
2007-02-28The right tactics for definitions using measures.msozeau
2007-02-27Fix wf bug from F. Besson and work on ineqs generation.msozeau
2007-02-27Revision of the coqide configuration: letouzey
2007-02-27Correction d'un bug de l'install (win)notin
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
2007-02-24Améliorations utiles pour les Makefile répartis sur plusieurs répertoiresherbelin
2007-02-24Opacity parameterization for obligations working.msozeau
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
2007-02-22Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeherbelin
2007-02-22Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...notin
2007-02-22doc: typo/english: "is left associating" -> "is left-associative".lmamane
2007-02-22Documentation of tactical "t1 || t2": t2 is executed if t1 fails tolmamane
2007-02-21Utilisation de l'environnement pour l'affichage de certains messages d'erreursherbelin
2007-02-21Correction typo liée au commit 8779 (levait une anomalie)herbelin
2007-02-21Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESherbelin
2007-02-21Removed some useless code in mod_typing that was redundant with safe_typing.soubiran
2007-02-21Fixed the pseudo-cicularity problem due to the with operator on Module Type.soubiran
2007-02-19Correct coq depend, add eq_rect elimination tactic to SubtacTacticsmsozeau
2007-02-19Ajouts de lemmes dans Min et Maxnotin
2007-02-19Various little subtac fixes, add some useful tactics.msozeau
2007-02-18Compilation de la FAQnotin
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
2007-02-16Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.msozeau
2007-02-16Missing keywordmsozeau
2007-02-16lift params appropriately, do not need to coerce to tyconmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 00:04:34 +0000