index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
hiddentac.ml
Commit message (
Expand
)
Author
Age
...
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
more evar stuff
corbinea
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
bugs avec Pose et Assert
barras
2004-01-09
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Added Instantiate ... in
corbinea
2003-11-06
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
*** empty log message ***
barras
2003-03-12
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
entetes
filliatr
2001-03-15
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations
filliatr
1999-11-24
*
modules Indrec, Tacentries, Hiddentac
filliatr
1999-11-23
[prev]