X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.mli;h=bc174d12196e50d2df8be84af126e18e84c87e4b;hb=c75bfdd4162050012614b70a68eff57fc3eabcc4;hp=a07b9d2979b9f4f702d163a5cf4bfce4b3ae5d02;hpb=7e60b896247a228beea1b2a547c1f606e1834921;p=helm.git diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli index a07b9d297..bc174d121 100644 --- a/helm/gTopLevel/cic2acic.mli +++ b/helm/gTopLevel/cic2acic.mli @@ -39,6 +39,7 @@ val acic_of_cic_context' : (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) Cic.metasenv -> (* metasenv *) Cic.context -> (* context *) + Cic.id list -> (* idrefs *) Cic.term -> (* term *) Cic.term option -> (* expected type *) Cic.annterm (* annotated term *)