aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* bug serieux efficacite de ltacGravatar barras2006-06-19
* Updating documentation of replace and correcting a typo in error message of r...Gravatar jforest2006-06-12
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* reparation pour le bug #1072 (soufflee par J. Forest): Gravatar letouzey2006-06-06
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* "subst." works now even when it exists an hypothesis have the form "x=x" in t...Gravatar jforest2006-05-20
* encore un correctif sur le rewrite H in setoid: Gravatar letouzey2006-05-05
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Changement de comportement de rewrite: face a une egalité setoid, onGravatar letouzey2006-05-02