From 11912557b53b4d16d8d1685f020c5080d1746033 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 5 Mar 2019 14:31:30 -0500
Subject: Actually fix reification of literals

---
 src/Language.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/Language.v b/src/Language.v
index d3d417d35..a686a846b 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -1158,6 +1158,7 @@ Module Compilers.
       | Datatypes.None => idtac
       | ZRange.Build_zrange ?x ?y
         => require_primitive_const x; require_primitive_const y
+      | literal ?x => idtac
       | ?term => fail 0 "Not a known const:" term
       end.
     Ltac is_primitive_const term :=
@@ -1193,9 +1194,6 @@ Module Compilers.
         | Nat.max => then_tac Nat_max
         | Nat.pred => then_tac Nat_pred
         | S => then_tac Nat_succ
-        | @literal ?T
-          => let rT := base.reify T in
-             then_tac (@ident.Literal rT)
         | @Datatypes.nil ?T
           => let rT := base.reify T in
              then_tac (@ident.nil rT)
-- 
cgit v1.2.3