]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/acic2Procedural.mli
we aligned the implementation to the plmms08 paper
[helm.git] / helm / software / components / acic_procedural / acic2Procedural.mli
index f0016cce20c355ec8772769884d7fd110c4d6d6c..230e74f46e54121183a2e5fb90191029b298b9de 100644 (file)
@@ -25,7 +25,7 @@
 
 val procedural_of_acic_object:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
-   ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> 
+   ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> ?info:string ->
    ?depth:int -> ?flavour:Cic.object_flavour -> string -> Cic.annobj ->
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
@@ -38,3 +38,5 @@ val procedural_of_acic_term:
       (Cic.annterm, Cic.annterm,
        Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list
+
+val debug: bool ref