From e03b8b3e48d88ac84f9f92424e72361500b76a18 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 16 Apr 2002 08:33:53 +0000 Subject: [PATCH] type_of_aux' exported. --- helm/ocaml/cic_proof_checking/cicTypeChecker.mli | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 72dd63c57..329b05083 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -32,3 +32,8 @@ exception NotPositiveOccurrences of string exception NotWellFormedTypeOfInductiveConstructor of string exception WrongRequiredArgument of string val typecheck : UriManager.uri -> unit +val type_of: Cic.term -> Cic.term + +(* used only in the toplevel *) +(* type_of_aux' metasenv context term *) +val type_of_aux': (int * Cic.term) list -> Cic.term list -> Cic.term -> Cic.term -- 2.39.2