aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Prise en compte des variables de grammaires de tactiques et dédollarisation ...Gravatar herbelin2003-04-08
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* code mortGravatar herbelin2003-04-07
* Backtrack du commit de Christine, qui posait probleme avec FTCGravatar letouzey2003-04-03
* Extension de Replace aux égalités entre preuvesGravatar herbelin2003-04-01
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Ajout d'un message à FailTac; localisation des appels à des tactiques défi...Gravatar herbelin2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* Fixed Relative names not,iff in Camlp4 quotation.Gravatar corbinea2003-03-28
* Introducing Christine's Intuition1 and adding some invertible hyps.Gravatar corbinea2003-03-18
* *** empty log message ***Gravatar barras2003-03-12
* Changed Tauto so it displays less 'Unfold not iff'Gravatar corbinea2003-02-26
* Correction d'un bug introduit dans le backtracking d'occurrenceGravatar delahaye2003-02-13
* Chargement dynamique de .cmaGravatar delahaye2003-02-13
* Debugger plus informatifGravatar delahaye2003-02-13
* Suppression de l'élimination des existentiels dans LinearIntuition.Gravatar corbinea2003-02-05
* Un type "standardisé" pour new_hypGravatar herbelin2003-01-25
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
* Mauvais environnement d'évaluation pour les globauxGravatar herbelin2003-01-22
* Correction bug réecriture à la racine pour le sétoide Prop.Gravatar clrenard2003-01-22
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
* Mauvaise interprétatin de IdentArgTypeGravatar herbelin2003-01-20
* Protection contre les noms de tactiques inconnus; restriction exceptions ratt...Gravatar herbelin2003-01-20
* Petits bugsGravatar herbelin2003-01-20
* Utilisation d'une exception 'catchable'Gravatar herbelin2003-01-19
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Subst sur une hyp qui n'existe pas ne fait pas une anomalieGravatar barras2003-01-16
* correction de bug de Subst: ne faisait rien lorsque l'hypotheseGravatar barras2003-01-09
* Commentaires; optimisationGravatar herbelin2002-12-30
* Utilisation du second-ordre avec possibilité de K-rédex dans lemInvGravatar herbelin2002-12-24
* code mortGravatar herbelin2002-12-24
* Re-essai de forcer le terme réécrit à apparaître dans le butGravatar herbelin2002-12-23
* Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationGravatar herbelin2002-12-21
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* suite du commit precedentGravatar barras2002-12-19
* nouveau Subst:Gravatar barras2002-12-17
* Traitement spécial pour les types à l'internalisationGravatar herbelin2002-12-15
* Ajout du vernac Proof withGravatar gregoire2002-12-12
* Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)Gravatar herbelin2002-12-10
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Re-ajout constrInGravatar herbelin2002-11-14
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
* Raffinement de l'heuristique d'unification dans sig_clausale_formeGravatar herbelin2002-11-06
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et LocalGravatar herbelin2002-10-23