]> matita.cs.unibo.it Git - helm.git/tree - helm/EXPORT/exportcoq/
Unuseful code removed.
[helm.git] / helm / EXPORT / exportcoq /
drwxr-xr-x   ..
-rw-r--r-- 109 Makefile
-rwxr-xr-x 320 export_contrib_theory.sh
-rwxr-xr-x 321 export_theory_theory.sh
-rwxr-xr-x 475 exporttheories.sh
-rw-r--r-- 390 provacoq.v
-rw-r--r-- 956 provacoqArith.v
-rw-r--r-- 305 provacoqBool.v
-rw-r--r-- 504 provacoqInit.v
-rw-r--r-- 400 provacoqLists.v
-rw-r--r-- 513 provacoqLogic.v
-rw-r--r-- 624 provacoqReals.v
-rw-r--r-- 1297 provacoqRelations.v
-rw-r--r-- 1555 provacoqSets.v
-rw-r--r-- 266 provacoqSorting.v
-rw-r--r-- 83 provacoqTrees.v
-rw-r--r-- 508 provacoqZArith.v
-rw-r--r-- 266 provacoqcontribOmega.v
-rw-r--r-- 469 provacoqcontribRing.v