Eliminate the need for WeakVar decidable equality axiom
[coq-hetmet.git] / src /
drwxr-xr-x   ..
-rw-r--r-- 5341 Extraction-prefix.hs
-rw-r--r-- 5744 Extraction.v
-rw-r--r-- 19352 General.v
-rw-r--r-- 2299 HaskCore.v
-rw-r--r-- 4936 HaskCoreLiterals.v
-rw-r--r-- 11493 HaskCoreToWeak.v
-rw-r--r-- 5488 HaskCoreTypes.v
-rw-r--r-- 1263 HaskCoreVars.v
-rw-r--r-- 2890 HaskKinds.v
-rw-r--r-- 14157 HaskProof.v
-rw-r--r-- 9089 HaskProofToLatex.v
-rw-r--r-- 6118 HaskProofToStrong.v
-rw-r--r-- 5057 HaskStrong.v
-rw-r--r-- 28622 HaskStrongToProof.v
-rw-r--r-- 7654 HaskStrongToWeak.v
-rw-r--r-- 30300 HaskStrongTypes.v
-rw-r--r-- 7955 HaskWeak.v
-rw-r--r-- 5877 HaskWeakToCore.v
-rw-r--r-- 18992 HaskWeakToStrong.v
-rw-r--r-- 6959 HaskWeakTypes.v
-rw-r--r-- 4195 HaskWeakVars.v
-rw-r--r-- 21682 NaturalDeduction.v
-rw-r--r-- 5199 NaturalDeductionToLatex.v
-rw-r--r-- 8560 Preamble.v