aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Report correction bug #1289 dans trunk (r9435 pour branche v8.1)Gravatar herbelin2006-12-26
* remplacement d'un test d'egalite par un test de convertibilite dans injection...Gravatar jforest2006-12-22
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Ajout de dépliage de l'énoncé, si besoin est, dans apply inGravatar herbelin2006-11-10
* Correction d'un bug refineGravatar herbelin2006-11-10
* Quick hack to solve to complexity issue in function mark_occurGravatar herbelin2006-11-01
* Retour sur la modification apportée en r9289, et nouvelle correction du bug ...Gravatar notin2006-10-31
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Affichage d'un message d'erreur losque qu'une relation n'a pas été déclarÃ...Gravatar notin2006-10-26
* Petit bug apply inGravatar herbelin2006-10-26
* Correction d'une tentative incorrecte (révision 9266) de clarificationGravatar herbelin2006-10-25
* Insère une coercion vers Sortclass dans 'contradiction' si nécessaireGravatar herbelin2006-10-24
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
* Ajout de la tactique "apply in".Gravatar herbelin2006-10-24
* Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...Gravatar herbelin2006-10-24
* Fixed "Show intros" which did not look at hypothesis.Gravatar courtieu2006-10-23
* Correction du bug #1255 (réécriture setoid sous un produit)Gravatar notin2006-10-20
* affichage des ... dans les scriptsGravatar barras2006-10-16
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* Retour sur la suppression du pf_nf (trop d'exemples utilisent avecGravatar herbelin2006-10-03
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* Suppression de la comparaison (inutile) des paramètres globaux desGravatar herbelin2006-09-30
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* fixed error mesg in decl modeGravatar corbinea2006-09-26
* Permet a un unfold de recevoir ses occurences a travers une variable Ltac.Gravatar letouzey2006-09-25
* Correction bug #1229 (toplevel "unresolved evar" fled throughGravatar herbelin2006-09-23
* Ajout d'une valeur VList dans tacinterp pour permettre de cabler desGravatar herbelin2006-09-22
* Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...Gravatar herbelin2006-09-21
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Indentation + svnpropGravatar notin2006-09-12
* Correction bug d'ordonnancement des hyps d'induction dans induction/destructGravatar herbelin2006-09-01
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
* Bug in replace tactics introduced in r9073 (overlap between replace .. with a...Gravatar jforest2006-08-23
* Forgot a file in previous commit Gravatar jforest2006-08-22
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* corrects an error in the substitution of module paths inside tactics:Gravatar bertot2006-08-17
* Reparation bug Show intros: les hypothèses introduites précédemmentGravatar courtieu2006-07-28
* Correction du bug #1116 Gravatar jforest2006-07-20
* amelioration du comportement de induction (retour a la version V8.0)Gravatar jforest2006-07-18
* Correcting for bug #1167 Gravatar jforest2006-07-05
* Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'...Gravatar herbelin2006-06-27
* Suite utilisation hyp au lieu ident: donne la localisationnGravatar herbelin2006-06-23
* Correction ident -> hyp pour dinterpréter des identificateurs devant êt...Gravatar herbelin2006-06-23
* Préservation compatibilité interprétation quantified hypothesis (provisoir...Gravatar herbelin2006-06-23
* Nettoyage, uniformisationGravatar herbelin2006-06-22
* Harmonisation de l'interprétation des intropatternGravatar herbelin2006-06-21