diff options
| -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) |