| Commit message (Expand) | Author | Age |
* | Ajout de dépliage de l'énoncé, si besoin est, dans apply in | herbelin | 2006-11-10 |
* | Correction d'un bug refine | herbelin | 2006-11-10 |
* | Quick hack to solve to complexity issue in function mark_occur | herbelin | 2006-11-01 |
* | Retour sur la modification apportée en r9289, et nouvelle correction du bug ... | notin | 2006-10-31 |
* | simplif de la partie ML de ring/field | barras | 2006-10-27 |
* | Affichage d'un message d'erreur losque qu'une relation n'a pas été déclarÃ... | notin | 2006-10-26 |
* | Petit bug apply in | herbelin | 2006-10-26 |
* | Correction d'une tentative incorrecte (révision 9266) de clarification | herbelin | 2006-10-25 |
* | Insère une coercion vers Sortclass dans 'contradiction' si nécessaire | herbelin | 2006-10-24 |
* | Extension de la primitive ltac fresh pour qu'elle accepte une liste de | herbelin | 2006-10-24 |
* | Ajout de la tactique "apply in". | herbelin | 2006-10-24 |
* | Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén... | herbelin | 2006-10-24 |
* | Fixed "Show intros" which did not look at hypothesis. | courtieu | 2006-10-23 |
* | Correction du bug #1255 (réécriture setoid sous un produit) | notin | 2006-10-20 |
* | affichage des ... dans les scripts | barras | 2006-10-16 |
* | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey | 2006-10-05 |
* | Changement de comportement du [rewrite ... in H]: Coq échoue si H | notin | 2006-10-03 |
* | Retour sur la suppression du pf_nf (trop d'exemples utilisent avec | herbelin | 2006-10-03 |
* | Une passe sur l'injection et la discrimination... | herbelin | 2006-10-01 |
* | Suppression de la comparaison (inutile) des paramètres globaux des | herbelin | 2006-09-30 |
* | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras | 2006-09-26 |
* | fixed error mesg in decl mode | corbinea | 2006-09-26 |
* | Permet a un unfold de recevoir ses occurences a travers une variable Ltac. | letouzey | 2006-09-25 |
* | Correction bug #1229 (toplevel "unresolved evar" fled through | herbelin | 2006-09-23 |
* | Ajout d'une valeur VList dans tacinterp pour permettre de cabler des | herbelin | 2006-09-22 |
* | Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s... | herbelin | 2006-09-21 |
* | Declarative Proof Language: main commit | corbinea | 2006-09-20 |
* | Indentation + svnprop | notin | 2006-09-12 |
* | Correction bug d'ordonnancement des hyps d'induction dans induction/destruct | herbelin | 2006-09-01 |
* | improve the amount of information given by the Ltac tactic debugger | bertot | 2006-08-28 |
* | Bug in replace tactics introduced in r9073 (overlap between replace .. with a... | jforest | 2006-08-23 |
* | Forgot a file in previous commit | jforest | 2006-08-22 |
* | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest | 2006-08-22 |
* | corrects an error in the substitution of module paths inside tactics: | bertot | 2006-08-17 |
* | Reparation bug Show intros: les hypothèses introduites précédemment | courtieu | 2006-07-28 |
* | Correction du bug #1116 | jforest | 2006-07-20 |
* | amelioration du comportement de induction (retour a la version V8.0) | jforest | 2006-07-18 |
* | Correcting for bug #1167 | jforest | 2006-07-05 |
* | Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'... | herbelin | 2006-06-27 |
* | Suite utilisation hyp au lieu ident: donne la localisationn | herbelin | 2006-06-23 |
* | Correction ident -> hyp pour dinterpréter des identificateurs devant êt... | herbelin | 2006-06-23 |
* | Préservation compatibilité interprétation quantified hypothesis (provisoir... | herbelin | 2006-06-23 |
* | Nettoyage, uniformisation | herbelin | 2006-06-22 |
* | Harmonisation de l'interprétation des intropattern | herbelin | 2006-06-21 |
* | bug serieux efficacite de ltac | barras | 2006-06-19 |
* | Updating documentation of replace and correcting a typo in error message of r... | jforest | 2006-06-12 |
* | Changement du type d'argument 'TacticArgType X' en un type | herbelin | 2006-06-08 |
* | reparation pour le bug #1072 (soufflee par J. Forest): | letouzey | 2006-06-06 |
* | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
* | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |