diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-05 14:31:30 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-05 14:31:30 -0500 |
commit | 11912557b53b4d16d8d1685f020c5080d1746033 (patch) | |
tree | 13f72b4c3f4078548ea9bfadced996152b2b17b8 /src | |
parent | 9bd13e1e66b72ec985e907eb8befb8d394ed2ae0 (diff) |
Actually fix reification of literals
Diffstat (limited to 'src')
-rw-r--r-- | src/Language.v | 4 |
1 files changed, 1 insertions, 3 deletions
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) |