index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
dn.ml
Commit message (
Expand
)
Author
Age
*
Term dnets do no need to contain the afferent constr pattern in their nodes.
Pierre-Marie Pédrot
2014-03-03
*
Extruding code not depending of the functor argument in Termdn.
Pierre-Marie Pédrot
2014-03-03
*
Replacing arguments of Trie by a cancellable monoid.
Pierre-Marie Pédrot
2014-03-03
*
Documenting the Tries module, uniformizing the names according to
ppedrot
2013-05-09
*
Monomorphization (tactics)
ppedrot
2012-11-25
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-23
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Enhanced discrimination nets implementation, which can now work with
msozeau
2008-06-27
*
Nouvelle en-tête
herbelin
2004-07-16
*
entetes
filliatr
2001-03-15
*
Nettoyage
herbelin
2000-04-26
*
discriminations nets
filliatr
1999-11-19
*
introduction de Gset et Gmap pour Tlm puis Dn
filliatr
1999-11-18
*
- répertoire tactics/
filliatr
1999-10-22