Changeset 1959 for src/ASM/StatusProofs.ma

Timestamp:

May 16, 2012, 5:12:22 PM (8 years ago)

Author:

mulligan

Message:

Commented out diverging application of demodulation and closed goals with a daemon in order to get ASM/StatusProofs.ma to compile.

File:

• src/ASM/StatusProofs.ma (modified) (1 diff)

src/ASM/StatusProofs.ma

@@ -375 +375 @@
   cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
   cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
-  cases (get_index_v bool 4 nu ??) normalize nodelta try /demod/ try %
+  cases (get_index_v bool 4 nu ??) normalize nodelta
+  (* XXX: try /demod/ try % *)
+  cases daemon
 qed.