aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2004-07-02syntax compatibility fixcorbinea
2004-06-30instantiate entry: constr -> lconstrcorbinea
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-28more evar stuffcorbinea
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
2004-06-26effective evar refiningcorbinea
2004-06-02bug #787 de Rolandbarras
2004-06-02Clarify the distinction between quantified_hypothesis and declared_or_quantif...herbelin
2004-05-07Bug mauvais sigmaherbelin
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
2004-03-31Morphismes déclarés comme Lemma pas comme Definitionherbelin
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations uti...herbelin
2004-03-18Backtrack sur commit 1.20herbelin
2004-03-17Desactivation de la syntaxe v7 de Hint Rewrite en v8herbelin
2004-03-17Message d'erreurherbelin
2004-03-15bug d'Inversion #529 (pb avec ordre d'evaluation)barras
2004-03-15Nouvelle reparation pour Abstract en presence de variables de contexte: on co...herbelin
2004-03-13Backtrack sur la réparation de Abstract qui casse autre chose; le problème ...herbelin
2004-03-12Retablissement de la correction bug d'inversion faite dans la version 1.116 e...herbelin
2004-03-12Ne pas ajouter le contexte de section dans Abstract, il est deja inclus (avec...herbelin
2004-03-11code obsoleteherbelin
2004-03-11Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...herbelin
2004-03-10Ajout tactiques stepl et stepr de Nimègueherbelin
2004-03-10Correction bug internalisation 'context'herbelin
2004-03-09bug de l'inversion (coq-bugs #529)barras
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...herbelin
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...herbelin
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...herbelin
2004-03-01ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'herbelin
2004-03-01Correction sur commit précédent : Tactics.cut réduisait de manière inappr...herbelin
2004-03-01Ajout 'replace in'herbelin
2004-03-01Déplacement définition intro_pattern_expr dans Genargherbelin
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte des...herbelin
2004-03-01Déplacement définition intro_pattern_expr dans Genargherbelin
2004-02-26added breakpoints to help idecorbinea
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-02-12Typoherbelin
2004-02-12Plus d'explicitation d'un message d'erreurherbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...herbelin
2004-01-23Bug induction lors de types inductives avec parametresherbelin
2004-01-09bugs avec Pose et Assertbarras
2003-12-23Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...herbelin
2003-12-23*** empty log message ***barras
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-13Correction bug soumis par Yvesherbelin
2003-12-01Nouvelle tactique EExistsclrenard
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:09:38 +0000