* doubleTypeInference.ml* added. For now, it just computes the synthesized type.

[helm.git] / helm / gTopLevel / doubleTypeInference.mli

diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
new file mode 100644 (file)
index 0000000..4de5bc0
--- /dev/null
+++ b/helm/gTopLevel/doubleTypeInference.mli
@@ -0,0 +1,19 @@
+exception Impossible of int
+exception NotWellTyped of string
+exception WrongUriToConstant of string
+exception WrongUriToVariable of string
+exception WrongUriToMutualInductiveDefinitions of string
+exception ListTooShort
+exception RelToHiddenHypothesis
+
+type types = {synthesized : Cic.term ; expected : Cic.term};;
+
+module CicHash :
+  sig
+    type key = Cic.term
+    and 'a t
+    val find : 'a t -> key -> 'a
+  end
+
+val double_type_of :
+ Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t