]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/cic_proof_checking/
LetIn reduction (alias zeta-reduction) is now performed during whd.
[helm.git] / helm / ocaml / cic_proof_checking /
drwxr-xr-x   ..
-rw-r--r-- 18 .cvsignore
-rw-r--r-- 922 .depend
-rw-r--r-- 541 Makefile
-rw-r--r-- 7212 cicCooking.ml
-rw-r--r-- 1224 cicCooking.mli
-rw-r--r-- 8365 cicEnvironment.ml
-rw-r--r-- 4285 cicEnvironment.mli
-rw-r--r-- 2059 cicMiniReduction.ml
-rw-r--r-- 1025 cicMiniReduction.mli
-rw-r--r-- 8404 cicPp.ml
-rw-r--r-- 2154 cicPp.mli
-rw-r--r-- 10834 cicReduction.ml
-rw-r--r-- 1296 cicReduction.mli
-rw-r--r-- 4454 cicSubstitution.ml
-rw-r--r-- 1141 cicSubstitution.mli
-rw-r--r-- 49698 cicTypeChecker.ml
-rw-r--r-- 1364 cicTypeChecker.mli