diff options
Diffstat (limited to 'lib/serialize.mli')
| -rw-r--r-- | lib/serialize.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/lib/serialize.mli b/lib/serialize.mli index 00e95be2ed..2b1718bf76 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -15,8 +15,9 @@ type 'a call type unknown -val interp : interp_sty -> interp_rty call -val backto : backto_sty -> backto_rty call +val add : add_sty -> add_rty call +val edit_at : edit_at_sty -> edit_at_rty call +val query : query_sty -> query_rty call val goals : goals_sty -> goals_rty call val hints : hints_sty -> hints_rty call val status : status_sty -> status_rty call @@ -51,7 +52,7 @@ val to_feedback : xml -> feedback val is_feedback : xml -> bool val of_answer : 'a call -> 'a value -> xml -val to_answer : xml -> 'a call -> 'a value +val to_answer : 'a call -> xml -> 'a value (** * Debug printing *) |