X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.mli;h=230e74f46e54121183a2e5fb90191029b298b9de;hb=e7759b1c1f40380748ac052bce5b677bc8fd71cb;hp=d1ff6a0c20e18695ed4b5b504e96fde40a85888f;hpb=4db221ee87ba30f63db0ea32c98858041e8e6213;p=helm.git diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index d1ff6a0c2..230e74f46 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -23,11 +23,20 @@ * http://cs.unibo.it/helm/. *) -val acic2procedural: +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 -> ?info:string -> + ?depth:int -> ?flavour:Cic.object_flavour -> string -> Cic.annobj -> + (Cic.annterm, Cic.annterm, + Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) + GrafiteAst.statement list + +val procedural_of_acic_term: 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 -> string -> Cic.context -> Cic.annterm -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list +val debug: bool ref