aboutsummaryrefslogtreecommitdiff
path: root/src/tac2interp.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-29 15:19:30 +0200
committerPierre-Marie Pédrot2017-08-29 15:19:30 +0200
commitf6154c8a086faee725b4f41fb4b2586d7cb6c51d (patch)
treea0a1014646eb817b765b8262980f1bd06a8b2e0c /src/tac2interp.ml
parent9f79d601c0863d5144fc07c5cea0e03ef41d244b (diff)
Removing dead code for handling of array litterals.
Diffstat (limited to 'src/tac2interp.ml')
-rw-r--r--src/tac2interp.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 3e1a048d29..3490b1a2a8 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -79,9 +79,6 @@ let rec interp ist = function
let iter (_, e) = e.clos_env <- ist in
let () = List.iter iter fixs in
interp ist e
-| GTacArr el ->
- Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
- return (ValBlk (0, Array.of_list el))
| GTacCst (_, n, []) -> return (ValInt n)
| GTacCst (_, n, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->