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
*
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
*
Subst (tout court)
filliatr
2002-09-16
*
tactique Subst x1 ... xn
filliatr
2002-09-11
*
Code mort de AutoRewrite
herbelin
2002-09-09
*
correction de bugs:
barras
2002-08-16
*
AutoRewrite substitutive...
coq
2002-08-13
*
Renoncement Ă distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Branchement de Assert, Pose et LetTac sur l'algo de création de noms
herbelin
2002-07-30
*
correction bugs Tauto
courant
2002-07-19
*
tactique Subst
filliatr
2002-07-17
*
Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]
corbinea
2002-07-17
*
Bug dans la globalisation des arguments de tactiques primitives
herbelin
2002-07-16
*
Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait
courant
2002-07-15
*
Que la localisation des erreurs pour les tactiques atomiques marche
herbelin
2002-07-11
*
Hack pour autoriser les $n dans les Grammar tactic
herbelin
2002-07-03
*
Réparation de l'interprétation des fermetures (sans casser Field!)
herbelin
2002-06-13
*
Ajout coercion constr vers hyp quantifiée
herbelin
2002-06-06
*
Tentative de réparation d'un bug Omega: une variable de section qui après e...
herbelin
2002-06-06
*
Passage de PatternMatchingFailure vers UserError pour capture par tclFIRST
herbelin
2002-06-06
*
Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...
herbelin
2002-06-05
*
Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...
herbelin
2002-06-05
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Les VContext ne sont plus des fermetures (temporaire)
delahaye
2002-05-31
*
Nettoyage
herbelin
2002-05-30
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
RĂ©organisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Pour les tactiques dépendant de False
herbelin
2002-05-29
*
Correction of a bug in Intuition (no more decomposition of dependent pairs).
corbinea
2002-05-22
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Finalement VTactic est gardé pour y plonger les tactiques ML, le
herbelin
2002-05-15
*
- Changement de l'ordre de filtrage dans "Match Context"
herbelin
2002-05-14
*
ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite
barras
2002-05-14
[next]