From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 16 Apr 2002 08:33:53 +0000 (+0000)
Subject: type_of_aux' exported.
X-Git-Tag: V_0_3_0_debian_8~158
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e03b8b3e48d88ac84f9f92424e72361500b76a18

type_of_aux' exported.
---

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