cic_transformations factorized into cic_omdoc and cic_transformations.

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.mli

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
new file mode 100644 (file)
index 0000000..d7d06ae
--- /dev/null
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -0,0 +1,25 @@
+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};;
+
+module CicHash :
+  sig
+    type 'a t
+    val find : 'a t -> Cic.term -> 'a
+  end
+;;
+
+val double_type_of :
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types 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