diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 19:17:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-15 20:05:34 +0200 |
| commit | 98618cfb6b326b70da29348bc5d212e41086f473 (patch) | |
| tree | b47e7955c5c35f1c415c68fd6a2e97b5745fc32a /lib/richpp.ml | |
| parent | 2c1882815e7877bfc574f9f71eff6ce099145df5 (diff) | |
More parametric type for generalized XML.
Diffstat (limited to 'lib/richpp.ml')
| -rw-r--r-- | lib/richpp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml index 45173ff30..087c24729 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -17,7 +17,7 @@ type 'annotation located = { type 'a stack = | Leaf -| Node of string * 'a located gxml list * int * 'a stack +| Node of string * (string, 'a located) gxml list * int * 'a stack type 'a context = { mutable stack : 'a stack; |