]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/cic_omdoc/
We do not compute inner-types for the metasenv ==> we handle it in a particular
[helm.git] / helm / ocaml / cic_omdoc /
drwxr-xr-x   ..
-rw-r--r-- 18 .cvsignore
-rw-r--r-- 745 .depend
-rw-r--r-- 355 Makefile
-rw-r--r-- 17902 cic2acic.ml
-rw-r--r-- 2402 cic2acic.mli
-rw-r--r-- 34064 cic2content.ml
-rw-r--r-- 1166 cic2content.mli
-rw-r--r-- 4731 content.ml
-rw-r--r-- 4114 content.mli
-rw-r--r-- 6489 content2cic.ml
-rw-r--r-- 1660 content2cic.mli
-rw-r--r-- 5233 contentPp.ml
-rw-r--r-- 1042 contentPp.mli
-rw-r--r-- 25114 doubleTypeInference.ml
-rw-r--r-- 692 doubleTypeInference.mli
-rw-r--r-- 6545 eta_fixing.ml
-rw-r--r-- 1042 eta_fixing.mli