aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/contradiction.ml
Commit message (Expand)AuthorAge
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Insère une coercion vers Sortclass dans 'contradiction' si nécessaireGravatar herbelin2006-10-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
* Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteGravatar herbelin2003-10-18
* Pour les tactiques dépendant de FalseGravatar herbelin2002-05-29