projects / tatoo.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 273665d) | patch
1) modifie la definition de query_tree
authorHuibo SHI <shihuibo19@gmail.com>
Wed, 19 Mar 2014 16:57:09 +0000 (17:57 +0100)
committerHuibo SHI <shihuibo19@gmail.com>
Wed, 19 Mar 2014 16:57:09 +0000 (17:57 +0100)
commit333d2789a5dd6b7395b5fedbcdd670e103e0eb4b
tree45578293ac839523f32b91b695aaae8256de2f9btree | snapshot
parent273665d1294e6253fbd45137471e7dd568b38735commit | diff
1) modifie la definition de query_tree
2) ajout la definition de query_tree_desc
3) ajout la fonction mk_node pour initialiser la query_tree
4) mettre la fonction mk_node dans bon endroit.
src/query_tree.ml diff | blob | history
src/table.ml diff | blob | history
tests/tiny2.xml diff | blob | history
Tree Automata TOOlkit