From e011e7cd08af361cb5de9c953bfc58b4cd918308 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 11 Jun 2005 12:18:59 +0000 Subject: [PATCH] added an 'a parameter to mpresentation type so that it and boxes could be used in a mutual recursive fashoin (boxes inside mpresentation inside boxes ...) needed by cic_notation --- .../applyTransformation.ml | 4 +- helm/ocaml/cic_transformations/ast2pres.ml | 2 +- helm/ocaml/cic_transformations/ast2pres.mli | 2 +- helm/ocaml/cic_transformations/box.ml | 22 +- helm/ocaml/cic_transformations/box.mli | 2 + helm/ocaml/cic_transformations/boxPp.ml | 1 + helm/ocaml/cic_transformations/cic2Xml.ml | 1 - helm/ocaml/cic_transformations/cic2Xml.mli | 9 +- .../cic_transformations/content2pres.mli | 2 +- .../cic_transformations/mpresentation.ml | 223 ++++++++---------- .../cic_transformations/mpresentation.mli | 68 +++--- .../cic_transformations/sequent2pres.mli | 2 +- 12 files changed, 160 insertions(+), 178 deletions(-) diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 6c0b0cddf..57d26f168 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -34,8 +34,8 @@ (***************************************************************************) let mpres_document pres_box = - Ast2pres.add_xml_declaration - (Box.box2xml ~obj2xml:Mpresentation.print_mpres pres_box) + let obj2xml obj = Mpresentation.print_mpres (fun _ -> assert false) obj in + Ast2pres.add_xml_declaration (Box.box2xml ~obj2xml pres_box) let mml_of_cic_sequent metasenv sequent = let asequent,ids_to_terms, diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index f0f9d934f..c7a82e533 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -592,7 +592,7 @@ let add_xml_declaration stream = let ast2mpresXml ((ast, ids_to_uris) as arg) = let astBox = ast2astBox arg in let smallAst2mpresXml ast = - P.print_mpres (ast2mpres (ast, ids_to_uris)) + P.print_mpres (fun _ -> assert false) (ast2mpres (ast, ids_to_uris)) in (Box.box2xml ~obj2xml:smallAst2mpresXml astBox) diff --git a/helm/ocaml/cic_transformations/ast2pres.mli b/helm/ocaml/cic_transformations/ast2pres.mli index 20e909869..5b0e5a740 100644 --- a/helm/ocaml/cic_transformations/ast2pres.mli +++ b/helm/ocaml/cic_transformations/ast2pres.mli @@ -44,7 +44,7 @@ val ast2astBox: val ast2mpres: ?priority:int -> ?assoc:bool -> CicAst.term * (Cic.id, string) Hashtbl.t -> - Mpresentation.mpres + unit Mpresentation.mpres val add_xml_declaration: Xml.token Stream.t -> Xml.token Stream.t diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_transformations/box.ml index 386fabd0b..96c55b18a 100644 --- a/helm/ocaml/cic_transformations/box.ml +++ b/helm/ocaml/cic_transformations/box.ml @@ -39,6 +39,8 @@ type | Ink of attr | H of attr * ('expr box) list | V of attr * ('expr box) list + | HV of attr * ('expr box) list + | HOV of attr * ('expr box) list | Object of attr * 'expr | Action of attr * ('expr box) list @@ -51,6 +53,13 @@ let indent t = H([],[skip;t]);; (* BoxML prefix *) let prefix = "b";; + +let tag_of_box = function + | H _ -> "h" + | V _ -> "v" + | HV _ -> "hv" + | HOV _ -> "hov" + | _ -> assert false let box2xml ~obj2xml box = let rec aux = @@ -59,12 +68,11 @@ let box2xml ~obj2xml box = Text (attr,s) -> X.xml_nempty ~prefix "text" attr (X.xml_cdata s) | Space attr -> X.xml_empty ~prefix "space" attr | Ink attr -> X.xml_empty ~prefix "ink" attr - | H (attr,l) -> - X.xml_nempty ~prefix "h" attr - [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) - >] - | V (attr,l) -> - X.xml_nempty ~prefix "v" attr + | H (attr,l) + | V (attr,l) + | HV (attr,l) + | HOV (attr,l) as box -> + X.xml_nempty ~prefix (tag_of_box box) attr [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >] | Object (attr,m) -> @@ -82,6 +90,8 @@ let rec map f = function | (Ink _) as box -> box | H (attr, l) -> H (attr, List.map (map f) l) | V (attr, l) -> V (attr, List.map (map f) l) + | HV (attr, l) -> HV (attr, List.map (map f) l) + | HOV (attr, l) -> HOV (attr, List.map (map f) l) | Action (attr, l) -> Action (attr, List.map (map f) l) | Object (attr, obj) -> Object (attr, f obj) ;; diff --git a/helm/ocaml/cic_transformations/box.mli b/helm/ocaml/cic_transformations/box.mli index 8d65c27f0..296b14c15 100644 --- a/helm/ocaml/cic_transformations/box.mli +++ b/helm/ocaml/cic_transformations/box.mli @@ -39,6 +39,8 @@ type | Ink of attr | H of attr * ('expr box) list | V of attr * ('expr box) list + | HV of attr * ('expr box) list + | HOV of attr * ('expr box) list | Object of attr * 'expr | Action of attr * ('expr box) list diff --git a/helm/ocaml/cic_transformations/boxPp.ml b/helm/ocaml/cic_transformations/boxPp.ml index 073bf633d..fcc913421 100644 --- a/helm/ocaml/cic_transformations/boxPp.ml +++ b/helm/ocaml/cic_transformations/boxPp.ml @@ -36,6 +36,7 @@ let to_string object_to_string b = | Box.V (_,b::bl')::tl -> aux_h current_s [b] ; aux_h (String.make (String.length current_s) ' ') (Box.V([],bl')::tl) + | Box.HV _ :: _ | Box.HOV _ :: _ -> assert false (* not implemented *) | Box.Object (_,obj)::tl -> aux_h (current_s ^ (object_to_string obj)) tl | (Box.Action _)::tl -> assert false | (Box.Ink _)::tl -> aux_h (current_s ^ "----------") tl diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 759f630b4..1facd4fd9 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -25,7 +25,6 @@ (*CSC codice cut & paste da cicPp e xmlcommand *) -exception ImpossiblePossible;; exception NotImplemented;; let dtdname ~ask_dtd_to_the_getter dtd = diff --git a/helm/ocaml/cic_transformations/cic2Xml.mli b/helm/ocaml/cic_transformations/cic2Xml.mli index b714469ec..47202dd01 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.mli +++ b/helm/ocaml/cic_transformations/cic2Xml.mli @@ -23,23 +23,24 @@ * http://cs.unibo.it/helm/. *) -exception ImpossiblePossible exception NotImplemented val print_term : ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> - Cic.annterm -> Xml.token Stream.t + Cic.annterm -> + Xml.token Stream.t val print_object : UriManager.uri -> ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> ask_dtd_to_the_getter:bool -> - Cic.annobj -> Xml.token Stream.t * Xml.token Stream.t option + Cic.annobj -> + Xml.token Stream.t * Xml.token Stream.t option val print_inner_types : UriManager.uri -> ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types: (string, Cic2acic.anntypes) Hashtbl.t -> ask_dtd_to_the_getter:bool -> - Xml.token Stream.t + Xml.token Stream.t diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 90258270b..7511a527e 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -35,5 +35,5 @@ val content2pres: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.cobj -> - Mpresentation.mpres Box.box + unit Mpresentation.mpres Box.box diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index 9ba9d848e..05e76fcde 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -32,9 +32,7 @@ (* *) (**************************************************************************) -type - mpres = - (* token elements *) +type 'a mpres = Mi of attr * string | Mn of attr * string | Mo of attr * string @@ -42,34 +40,28 @@ type | Mspace of attr | Ms of attr * string | Mgliph of attr * string - (* General Layout Schemata *) - | Mrow of attr * mpres list - | Mfrac of attr * mpres * mpres - | Msqrt of attr * mpres - | Mroot of attr * mpres * mpres - | Mstyle of attr * mpres - | Merror of attr * mpres - | Mpadded of attr * mpres - | Mphantom of attr * mpres - | Mfenced of attr * mpres list - | Menclose of attr * mpres - (* Script and Limit Schemata *) - | Msub of attr * mpres * mpres - | Msup of attr * mpres * mpres - | Msubsup of attr * mpres * mpres *mpres - | Munder of attr * mpres * mpres - | Mover of attr * mpres * mpres - | Munderover of attr * mpres * mpres *mpres + | Mrow of attr * 'a mpres list + | Mfrac of attr * 'a mpres * 'a mpres + | Msqrt of attr * 'a mpres + | Mroot of attr * 'a mpres * 'a mpres + | Mstyle of attr * 'a mpres + | Merror of attr * 'a mpres + | Mpadded of attr * 'a mpres + | Mphantom of attr * 'a mpres + | Mfenced of attr * 'a mpres list + | Menclose of attr * 'a mpres + | Msub of attr * 'a mpres * 'a mpres + | Msup of attr * 'a mpres * 'a mpres + | Msubsup of attr * 'a mpres * 'a mpres *'a mpres + | Munder of attr * 'a mpres * 'a mpres + | Mover of attr * 'a mpres * 'a mpres + | Munderover of attr * 'a mpres * 'a mpres *'a mpres (* | Multiscripts of ??? NOT IMPLEMEMENTED *) - (* Tables and Matrices *) - | Mtable of attr * row list - (* Enlivening Expressions *) - | Maction of attr * mpres list - -and row = Mtr of attr * mtd list - -and mtd = Mtd of attr * mpres - + | Mtable of attr * 'a row list + | Maction of attr * 'a mpres list + | Mobject of attr * 'a +and 'a row = Mtr of attr * 'a mtd list +and 'a mtd = Mtd of attr * 'a mpres and attr = (string option * string * string) list ;; @@ -110,104 +102,77 @@ let row_without_brackets attr a b op = (* MathML prefix *) let prefix = "m";; -let rec print_mpres = - let module X = Xml in - function - Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s) - | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s) - | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s) - | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s) - | Mspace attr -> X.xml_empty ~prefix "mspace" attr - | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s) - | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s) - (* General Layout Schemata *) - | Mrow (attr,l) -> - X.xml_nempty ~prefix "mrow" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - | Mfrac (attr,m1,m2) -> - X.xml_nempty ~prefix "mfrac" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msqrt (attr,m) -> - X.xml_nempty ~prefix "msqrt" attr [< print_mpres m >] - | Mroot (attr,m1,m2) -> - X.xml_nempty ~prefix "mroot" attr - [< print_mpres m1; - print_mpres m2 - >] - | Mstyle (attr,m) -> - X.xml_nempty ~prefix "mstyle" attr [< print_mpres m >] - | Merror (attr,m) -> - X.xml_nempty ~prefix "merror" attr [< print_mpres m >] - | Mpadded (attr,m) -> - X.xml_nempty ~prefix "mpadded" attr [< print_mpres m >] - | Mphantom (attr,m) -> - X.xml_nempty ~prefix "mphantom" attr [< print_mpres m >] - | Mfenced (attr,l) -> - X.xml_nempty ~prefix "mfenced" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - | Menclose (attr,m) -> - X.xml_nempty ~prefix "menclose" attr [< print_mpres m >] - (* Script and Limit Schemata *) - | Msub (attr,m1,m2) -> - X.xml_nempty ~prefix "msub" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msup (attr,m1,m2) -> - X.xml_nempty ~prefix "msup" attr - [< print_mpres m1; - print_mpres m2 - >] - | Msubsup (attr,m1,m2,m3) -> - X.xml_nempty ~prefix "msubsup" attr - [< print_mpres m1; - print_mpres m2; - print_mpres m3 - >] - | Munder (attr,m1,m2) -> - X.xml_nempty ~prefix "munder" attr - [< print_mpres m1; - print_mpres m2 - >] - | Mover (attr,m1,m2) -> - X.xml_nempty ~prefix "mover" attr - [< print_mpres m1; - print_mpres m2 - >] - | Munderover (attr,m1,m2,m3) -> - X.xml_nempty ~prefix "munderover" attr - [< print_mpres m1; - print_mpres m2; - print_mpres m3 - >] -(* | Multiscripts of ??? NOT IMPLEMEMENTED *) - (* Tables and Matrices *) - | Mtable (attr, rl) -> - X.xml_nempty ~prefix "mtable" attr - [< (List.fold_right (fun x i -> [< (print_mrow x) ; i >]) rl [<>]) - >] - (* Enlivening Expressions *) - | Maction (attr, l) -> - X.xml_nempty ~prefix "maction" attr - [< (List.fold_right (fun x i -> [< (print_mpres x) ; i >]) l [<>]) - >] - -and print_mrow = +let print_mpres obj_printer mpres = let module X = Xml in - function - Mtr (attr, l) -> - X.xml_nempty ~prefix "mtr" attr - [< (List.fold_right (fun x i -> [< (print_mtd x) ; i >]) l [<>]) - >] - -and print_mtd = - let module X = Xml in - function - Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] + let rec aux = + function + Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s) + | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s) + | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s) + | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s) + | Mspace attr -> X.xml_empty ~prefix "mspace" attr + | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s) + | Mgliph (attr,s) -> X.xml_nempty ~prefix "mgliph" attr (X.xml_cdata s) + (* General Layout Schemata *) + | Mrow (attr,l) -> + X.xml_nempty ~prefix "mrow" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) + >] + | Mfrac (attr,m1,m2) -> + X.xml_nempty ~prefix "mfrac" attr [< aux m1; aux m2 >] + | Msqrt (attr,m) -> + X.xml_nempty ~prefix "msqrt" attr [< aux m >] + | Mroot (attr,m1,m2) -> + X.xml_nempty ~prefix "mroot" attr [< aux m1; aux m2 >] + | Mstyle (attr,m) -> X.xml_nempty ~prefix "mstyle" attr [< aux m >] + | Merror (attr,m) -> X.xml_nempty ~prefix "merror" attr [< aux m >] + | Mpadded (attr,m) -> X.xml_nempty ~prefix "mpadded" attr [< aux m >] + | Mphantom (attr,m) -> X.xml_nempty ~prefix "mphantom" attr [< aux m >] + | Mfenced (attr,l) -> + X.xml_nempty ~prefix "mfenced" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) + >] + | Menclose (attr,m) -> X.xml_nempty ~prefix "menclose" attr [< aux m >] + (* Script and Limit Schemata *) + | Msub (attr,m1,m2) -> + X.xml_nempty ~prefix "msub" attr [< aux m1; aux m2 >] + | Msup (attr,m1,m2) -> + X.xml_nempty ~prefix "msup" attr [< aux m1; aux m2 >] + | Msubsup (attr,m1,m2,m3) -> + X.xml_nempty ~prefix "msubsup" attr [< aux m1; aux m2; aux m3 >] + | Munder (attr,m1,m2) -> + X.xml_nempty ~prefix "munder" attr [< aux m1; aux m2 >] + | Mover (attr,m1,m2) -> + X.xml_nempty ~prefix "mover" attr [< aux m1; aux m2 >] + | Munderover (attr,m1,m2,m3) -> + X.xml_nempty ~prefix "munderover" attr [< aux m1; aux m2; aux m3 >] + (* | Multiscripts of ??? NOT IMPLEMEMENTED *) + (* Tables and Matrices *) + | Mtable (attr, rl) -> + X.xml_nempty ~prefix "mtable" attr + [< (List.fold_right (fun x i -> [< (aux_mrow x) ; i >]) rl [<>]) >] + (* Enlivening Expressions *) + | Maction (attr, l) -> + X.xml_nempty ~prefix "maction" attr + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>]) >] + | Mobject (attr, obj) -> + X.xml_nempty ~prefix "msemantics" attr (obj_printer obj) + and aux_mrow = + let module X = Xml in + function + Mtr (attr, l) -> + X.xml_nempty ~prefix "mtr" attr + [< (List.fold_right (fun x i -> [< (aux_mtd x) ; i >]) l [<>]) + >] + and aux_mtd = + let module X = Xml in + function + Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr + [< (aux m) ; + X.xml_nempty ~prefix "mphantom" [] + (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >] + in + aux mpres ;; let document_of_mpres pres = @@ -217,7 +182,7 @@ let document_of_mpres pres = [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ; Some "xmlns","helm","http://www.cs.unibo.it/helm" ; Some "xmlns","xlink","http://www.w3.org/1999/xlink" - ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres)) + ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, + "rowspacing", "0.6ex"] (print_mpres (fun _ -> assert false) pres)) >] - diff --git a/helm/ocaml/cic_transformations/mpresentation.mli b/helm/ocaml/cic_transformations/mpresentation.mli index 83f243e6d..60ba3c9e1 100644 --- a/helm/ocaml/cic_transformations/mpresentation.mli +++ b/helm/ocaml/cic_transformations/mpresentation.mli @@ -23,8 +23,7 @@ * http://cs.unibo.it/helm/. *) -type - mpres = +type 'a mpres = (* token elements *) Mi of attr * string | Mn of attr * string @@ -34,45 +33,50 @@ type | Ms of attr * string | Mgliph of attr * string (* General Layout Schemata *) - | Mrow of attr * mpres list - | Mfrac of attr * mpres * mpres - | Msqrt of attr * mpres - | Mroot of attr * mpres * mpres - | Mstyle of attr * mpres - | Merror of attr * mpres - | Mpadded of attr * mpres - | Mphantom of attr * mpres - | Mfenced of attr * mpres list - | Menclose of attr * mpres + | Mrow of attr * 'a mpres list + | Mfrac of attr * 'a mpres * 'a mpres + | Msqrt of attr * 'a mpres + | Mroot of attr * 'a mpres * 'a mpres + | Mstyle of attr * 'a mpres + | Merror of attr * 'a mpres + | Mpadded of attr * 'a mpres + | Mphantom of attr * 'a mpres + | Mfenced of attr * 'a mpres list + | Menclose of attr * 'a mpres (* Script and Limit Schemata *) - | Msub of attr * mpres * mpres - | Msup of attr * mpres * mpres - | Msubsup of attr * mpres * mpres *mpres - | Munder of attr * mpres * mpres - | Mover of attr * mpres * mpres - | Munderover of attr * mpres * mpres *mpres -(* | Multiscripts of ??? NOT IMPLEMEMENTED *) + | Msub of attr * 'a mpres * 'a mpres + | Msup of attr * 'a mpres * 'a mpres + | Msubsup of attr * 'a mpres * 'a mpres *'a mpres + | Munder of attr * 'a mpres * 'a mpres + | Mover of attr * 'a mpres * 'a mpres + | Munderover of attr * 'a mpres * 'a mpres *'a mpres (* Tables and Matrices *) - | Mtable of attr * row list + | Mtable of attr * 'a row list (* Enlivening Expressions *) - | Maction of attr * mpres list + | Maction of attr * 'a mpres list + (* Embedding *) + | Mobject of attr * 'a -and row = Mtr of attr * mtd list +and 'a row = Mtr of attr * 'a mtd list -and mtd = Mtd of attr * mpres +and 'a mtd = Mtd of attr * 'a mpres and attr = (string option * string * string) list ;; -val smallskip : mpres -val indented : mpres -> mpres +val smallskip : 'a mpres +val indented : 'a mpres -> 'a mpres val standard_tbl_attr : attr -val two_rows_table : attr -> mpres -> mpres -> mpres -val two_rows_table_with_brackets : attr -> mpres -> mpres -> mpres -> mpres -val two_rows_table_without_brackets : attr -> mpres -> mpres -> mpres -> mpres -val row_with_brackets : attr -> mpres -> mpres -> mpres -> mpres -val row_without_brackets : attr -> mpres -> mpres -> mpres -> mpres -val print_mpres : mpres -> Xml.token Stream.t -val document_of_mpres : mpres -> Xml.token Stream.t +val two_rows_table : attr -> 'a mpres -> 'a mpres -> 'a mpres +val two_rows_table_with_brackets : + attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres +val two_rows_table_without_brackets : + attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres +val row_with_brackets : + attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres +val row_without_brackets : + attr -> 'a mpres -> 'a mpres -> 'a mpres -> 'a mpres +val print_mpres : ('a -> Xml.token Stream.t) -> 'a mpres -> Xml.token Stream.t +val document_of_mpres : 'a mpres -> Xml.token Stream.t diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli index 7a6d8ead3..e1c9da1dd 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.mli +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -35,5 +35,5 @@ val sequent2pres : ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.conjecture -> - Mpresentation.mpres Box.box + unit Mpresentation.mpres Box.box -- 2.39.2