added some flags to render subproofs (an hack)

[helm.git] / components / acic_procedural / acic2Procedural.mli

diff --git a/components/acic_procedural/acic2Procedural.mli b/components/acic_procedural/acic2Procedural.mli
index d1ff6a0c20e18695ed4b5b504e96fde40a85888f..35092fb16099d1279263bf181b5b969b460b994e 100644 (file)
--- a/components/acic_procedural/acic2Procedural.mli
+++ b/components/acic_procedural/acic2Procedural.mli
@@ -26,7 +26,8 @@
 val acic2procedural:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
    ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
-   ?depth:int -> string -> Cic.annobj ->
+   ?depth:int -> ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->
+     string -> Cic.annobj ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list