X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_acic%2FdoubleTypeInference.mli;fp=components%2Fcic_acic%2FdoubleTypeInference.mli;h=dcc7b66bd19f6e6821b6651b2e527f9b55cab1a7;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/cic_acic/doubleTypeInference.mli b/components/cic_acic/doubleTypeInference.mli
new file mode 100644
index 000000000..dcc7b66bd
--- /dev/null
+++ b/components/cic_acic/doubleTypeInference.mli
@@ -0,0 +1,21 @@
+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 option};;
+
+val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
+
+val double_type_of :
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
+  types Cic.CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool