]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/cic_unification/
- refine's type_of no longer return a substitution
[helm.git] / helm / ocaml / cic_unification /
drwxr-xr-x   ..
-rw-r--r-- 18 .cvsignore
-rw-r--r-- 625 .depend
-rw-r--r-- 280 Makefile
-rw-r--r-- 21035 cicMetaSubst.ml
-rw-r--r-- 3254 cicMetaSubst.mli
-rw-r--r-- 8687 cicMkImplicit.ml
-rw-r--r-- 1555 cicMkImplicit.mli
-rw-r--r-- 21475 cicRefine.ml
-rw-r--r-- 1479 cicRefine.mli
-rw-r--r-- 9900 cicUnification.ml
-rw-r--r-- 2308 cicUnification.mli