Changeset 1923 for src/ASM/CostsProof.ma

Timestamp:

May 8, 2012, 3:43:37 PM (8 years ago)

Author:

mulligan

Message:

Small change, closing daemon that went under the RADAR

File:

• src/ASM/CostsProof.ma (modified) (3 diffs)

src/ASM/CostsProof.ma

@@ -675 +675 @@
   |8:
     #end_flag #start_status #end_status #trace_any_label #costed_assm
-    #unrepeating_witness
+    #unrepeating_witness'
     whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
     >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
@@ -687 +687 @@
         generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
         normalize in match (nth_safe ? ? ? ?);
-        whd in costed_assm; lapply costed_assm -costed_assm    
+        whd in costed_assm; lapply costed_assm  
         inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
         [1:
@@ -698 +698 @@
           #cost -block_cost_assm #block_cost_assm
           cases (block_cost_assm ??? trace_any_label ???)
-          try @refl
-          [1:
-            assumption
-          |2:
-            (* XXX: !!! *)
-            cases daemon
-          ]
+          try @refl assumption
         ]
       ]