index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.ml
Commit message (
Expand
)
Author
Age
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramĂ...
herbelin
2004-01-27
*
Bug induction lors de types inductives avec parametres
herbelin
2004-01-23
*
bugs avec Pose et Assert
barras
2004-01-09
*
Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...
herbelin
2003-12-23
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Bug nommage destruct
herbelin
2003-11-15
*
Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste
herbelin
2003-11-14
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Idtac peut prendre un argument Ă afficher
narboux
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...
herbelin
2003-11-09
*
Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...
herbelin
2003-10-21
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
Typo
herbelin
2003-10-10
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Correction bug NewInduction pour les inductifs de type 'ordinaux'
herbelin
2003-09-23
*
Indépendance vis à vis de Declare
herbelin
2003-09-12
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Backtrack du commit de Christine, qui posait probleme avec FTC
letouzey
2003-04-03
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Commentaires; optimisation
herbelin
2002-12-30
*
code mort
herbelin
2002-12-24
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)
herbelin
2002-12-10
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
JMeq now treated as an equality by tactics.
courant
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
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
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
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
*
Tentative de réparation d'un bug Omega: une variable de section qui après e...
herbelin
2002-06-06
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
labels appliques dans un ordre incorrect
barras
2002-03-01
*
Uniformisation convert_hyp; correction problème de dépendance dans letin_tac
herbelin
2002-02-28
*
suppression de pop_named
barras
2002-02-22
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
[next]