From: Kim Nguyễn <kim.nguyen@lri.fr>
Date: Tue, 18 Apr 2017 12:53:58 +0000 (+0200)
Subject: Merge branch 'jit' of ssh://git.nguyen.vg/tatoo into jit
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=f075cc700c848d75d941e11eda36380e1760d0d9;hp=6bf7e46a9e33989261c349cbe532c6eec1585427

Merge branch 'jit' of ssh://git.nguyen.vg/tatoo into jit
---

diff --git a/src/tree.ml b/src/tree.ml
index 2696707..a1cd6a1 100644
--- a/src/tree.ml
+++ b/src/tree.ml
@@ -157,5 +157,4 @@ sig
   *)
   val print_node : Format.formatter -> node -> unit
 
-  val dispatch ('a -> 'b -> QName.t -> NodeSummary.t -> node -> node 
 end