Remove dead code in rebuild-reified.py

mit-plv · Nov 11, 2016 · d90c24f · d90c24f
1 parent e9c5dda
commit d90c24f
Showing 1 changed file with 0 additions and 9 deletions.
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -14,15 +14,6 @@
   := Expr%(uopkind)s_correct_and_bounded
        r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
        _ _.
-""" % locals()
-    elif name == 'Freeze':
-        extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
-Axiom proof_admitted : False.
-(** XXX TODO: Fix bounds analysis on freeze *)
-Definition r%(lname)sW_correct_and_bounded
-  := Expr%(uopkind)s_correct_and_bounded
-       r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
-       match proof_admitted with end match proof_admitted with end.
 """ % locals()
     with open(name.replace('_', '') + '.v', 'w') as f:
         f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common%(uopkind)s.