index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
funind
/
tacinvutils.ml
Age
Commit message (
Expand
)
Author
2008-04-28
menage dans funind + deplaceemnt de recdef dans funind
jforest
2006-09-20
Declarative Proof Language: main commit
corbinea
2006-01-11
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2005-12-02
Changement des named_context
gregoire
2005-05-26
Correction of a bug in functional scheme. It raised with mutual
coq
2005-02-12
Uniformisation de destApplication en destApp
herbelin
2004-12-10
Hugo fixed a bug of refine, and it revealed a bug of functional
coq
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-02-09
New version of Functional Scheme and functional induction. Deals with
coq
2003-09-12
Simplification vis a vis de Declare
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-03-31
Correcting a bug occuring when the mimicked function had a
courtieu
2003-03-31
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-02-27
The contribution of Pierre Courtieu on generating specialized induction schemes
bertot
