index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Changed Tauto so it displays less 'Unfold not iff'
corbinea
2003-02-26
*
Correction d'un bug introduit dans le backtracking d'occurrence
delahaye
2003-02-13
*
Chargement dynamique de .cma
delahaye
2003-02-13
*
Debugger plus informatif
delahaye
2003-02-13
*
Suppression de l'élimination des existentiels dans LinearIntuition.
corbinea
2003-02-05
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).
corbinea
2003-01-23
*
Mauvais environnement d'évaluation pour les globaux
herbelin
2003-01-22
*
Correction bug réecriture à la racine pour le sétoide Prop.
clrenard
2003-01-22
*
Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur
herbelin
2003-01-21
*
Mauvaise interprétatin de IdentArgType
herbelin
2003-01-20
*
Protection contre les noms de tactiques inconnus; restriction exceptions ratt...
herbelin
2003-01-20
*
Petits bugs
herbelin
2003-01-20
*
Utilisation d'une exception 'catchable'
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Subst sur une hyp qui n'existe pas ne fait pas une anomalie
barras
2003-01-16
*
correction de bug de Subst: ne faisait rien lorsque l'hypothese
barras
2003-01-09
*
Commentaires; optimisation
herbelin
2002-12-30
*
Utilisation du second-ordre avec possibilité de K-rédex dans lemInv
herbelin
2002-12-24
*
code mort
herbelin
2002-12-24
*
Re-essai de forcer le terme réécrit à apparaître dans le but
herbelin
2002-12-23
*
Backtrack sur la tentative d'interdire les K-abstractions dans l'unification
herbelin
2002-12-21
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
suite du commit precedent
barras
2002-12-19
*
nouveau Subst:
barras
2002-12-17
*
Traitement spécial pour les types à l'internalisation
herbelin
2002-12-15
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)
herbelin
2002-12-10
*
Option pour rendre les vérifications du refiner optionnelle
herbelin
2002-12-09
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Re-ajout constrIn
herbelin
2002-11-14
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
JMeq now treated as an equality by tactics.
courant
2002-11-14
*
Raffinement de l'heuristique d'unification dans sig_clausale_forme
herbelin
2002-11-06
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local
herbelin
2002-10-23
*
Correction d'une incompatibilité de nommage introduite lors du commit précÃ...
herbelin
2002-10-22
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
L'application de ltac attend une référence; meilleure protection contre
herbelin
2002-10-14
*
Réparation bug Inversion (#212)
herbelin
2002-10-14
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Subst ne fait pas clear sur x:=e
filliatr
2002-10-08
*
Oops...
coq
2002-10-01
*
Table fonctionnelle dans autorewrite
coq
2002-10-01
*
Vraie substitutivite de autohints
coq
2002-10-01
*
bug de noms long pour eqT.
clrenard
2002-10-01
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
passage a ocaml 3.06
herbelin
2002-09-27
[next]