aboutsummaryrefslogtreecommitdiff
path: root/tactics/dn.ml
AgeCommit message (Expand)Author
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-09-18Clean up a bit the implemenation of dnets.Pierre-Marie Pédrot
2020-09-18Remove dead code in dnets.Pierre-Marie Pédrot
2020-07-27Do not rely on higher-order interfaces for patterns in dnets.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2015-04-16Ensuring purity of datastructures in the API.Pierre-Marie Pédrot
2014-03-03Term dnets do no need to contain the afferent constr pattern in their nodes.Pierre-Marie Pédrot
2014-03-03Extruding code not depending of the functor argument in Termdn.Pierre-Marie Pédrot
2014-03-03Replacing arguments of Trie by a cancellable monoid.Pierre-Marie Pédrot
2013-05-09Documenting the Tries module, uniformizing the names according toppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2004-07-16Nouvelle en-têteherbelin
2001-03-15entetesfilliatr
2000-04-26Nettoyageherbelin
1999-11-19discriminations netsfilliatr
1999-11-18introduction de Gset et Gmap pour Tlm puis Dnfilliatr
1999-10-22 - répertoire tactics/filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:42:51 +0000