aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-02-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5296 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04Reconnaissance précoce de la dépendance du prédicat en un terme filtréherbelin
dans le cas v8 (build_initial_predicate au lieu de expand_arg); Correction d'un bug en présence de termes de type non inductif (cf success/Case15.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04Vérification de la prise en compte des termes de type non inductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5294 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04clean-ide plus precisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5293 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais ↵herbelin
reste a transporter les loc dans check_fix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5292 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04Boite autour des quote pour eviter un retour a la ligne apres le premier ↵herbelin
guillement; quote seulement en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5291 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04bug fix find coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5290 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04highlightmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04search windowcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5287 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5286 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Relachement condition pour afficher @ en cas d'explicitation d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5285 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Relachement condition pour declarer un inductif dans la table des 'If'; ↵herbelin
contrainte de non dependances en les args des constructeurs pour avoir un affichage spontane avec if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5284 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ↵herbelin
des dependances de nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Bug focusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5282 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Protection contre noms de variable indefinis et guillemets autour des constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5281 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un ↵herbelin
nom doit filtrer un nom et anonymous doit filtrer anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5280 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5279 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02reorganize the order of librairies in the entry CMO to make sure this canbertot
be used as a reference to know in which order the libraries should be loaded git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5278 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
uncapitalizes dependentrewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5277 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5276 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5275 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30updates the definition of tactics using Ltac and adds the subst tacticbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5274 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30adds module commands and update the extration commandbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5273 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5272 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5271 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29pour win32coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5270 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute ↵herbelin
fonctionnalite de haut niveau de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant ↵herbelin
que les variables liees sont toujours nommees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29pour ide sous windowscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5266 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Suppression de 'Print.' en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵herbelin
:= c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29updates the tactics contradiction and autorewrite, the commandsbertot
set implicit arguments, hint rewrite, and proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5262 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28Bug de Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5261 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28make sure that 'in' clauses for reduction tactics are translatedbertot
once again re-organize the way intro patterns are translated: there is now only one kind of pattern that can be used for both and and or constructs: the use of the multiplet notation should only be a matter of notation. un-capitalize a few tactic names for tactics represented using the TacExtend construct. corrects a bug in the way binders or coercion binders were used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5259 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5258 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Bug activation erronée du traducteur en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5257 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27meilleure separation de compil et install de coq, coqide et coq-interfacebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5256 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Correction des cibles des theories indviduellesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5255 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27MAJ simplificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5254 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5253 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵herbelin
paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5251 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5250 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26deplacement des cma et cmxa dans les sous-repertoiresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26reparation de qqs bugs du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26a try to make intro patterns betterbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5247 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 04:10:13 +0000