X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.mli;h=5f7e3ae97e06c14882d5362a70f844eff0107502;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=95ee658c7de98b637cc10261e8b6317efa4d3959;hpb=e4525d2a61f8bc9967d165d7bfd710037fb09d79;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 95ee658c7..5f7e3ae97 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -27,13 +27,13 @@ exception TypeCheckerFailure of string exception AssertFailure of string -val typecheck : UriManager.uri -> unit +val typecheck : UriManager.uri -> Cic.obj (* FUNCTIONS USED ONLY IN THE TOPLEVEL *) (* type_of_aux' metasenv context term *) val type_of_aux': - Cic.metasenv -> Cic.context -> Cic.term -> Cic.term + ?subst:Cic.substitution -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term (* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *) val typecheck_mutual_inductive_defs :