]> matita.cs.unibo.it Git - helm.git/tree - helm/software/components/ng_refiner/
1) unification hint now takes NG terms (as it should have been from the very
[helm.git] / helm / software / components / ng_refiner /
drwxr-xr-x   ..
-rw-r--r-- 1219 .depend
-rw-r--r-- 1219 .depend.opt
-rw-r--r-- 2140 Makefile
-rw-r--r-- 11822 check.ml
-rw-r--r-- 2754 esempio.ma
-rw-r--r-- 4334 nCicCoercion.ml
-rw-r--r-- 1367 nCicCoercion.mli
-rw-r--r-- 19410 nCicMetaSubst.ml
-rw-r--r-- 2903 nCicMetaSubst.mli
-rw-r--r-- 32102 nCicRefiner.ml
-rw-r--r-- 1250 nCicRefiner.mli
-rw-r--r-- 8014 nCicUnifHint.ml
-rw-r--r-- 1093 nCicUnifHint.mli
-rw-r--r-- 25839 nCicUnification.ml
-rw-r--r-- 2484 nCicUnification.mli
-rw-r--r-- 2808 nDiscriminationTree.ml
-rw-r--r-- 1372 nDiscriminationTree.mli
-rw-r--r-- 1053 nRstatus.ml
-rw-r--r-- 1044 nRstatus.mli
-rw-r--r-- 229 oMeta2nMeta.ml
-rw-r--r-- 1733 rt.ml