Removing dead code for handling of array litterals.

5 files changed, 3 insertions, 11 deletions

diff --git a/src/tac2env.ml b/src/tac2env.ml
index 59344e336b..dd8a07ffc6 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -65,7 +65,7 @@ let rec eval_pure = function
 | GTacCst (_, n, []) -> ValInt n
 | GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el)
 | GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_pure el)
-| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _
+| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _
 | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
   anomaly (Pp.str "Term is not a syntactical value")
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 0c9112d902..42203a32e5 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -126,7 +126,6 @@ type glb_tacexpr =
 | GTacFun of Name.t list * glb_tacexpr
 | GTacApp of glb_tacexpr * glb_tacexpr list
 | GTacLet of rec_flag * (Name.t * glb_tacexpr) list * glb_tacexpr
-| GTacArr of glb_tacexpr list
 | GTacCst of case_info * int * glb_tacexpr list
 | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array
 | GTacPrj of type_constant * glb_tacexpr * int
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 9d22b18af4..02dfa1c08b 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -416,13 +416,13 @@ let rec is_value = function
 | GTacCst (_, _, []) -> true
 | GTacOpn (_, el) -> List.for_all is_value el
 | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
-| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
+| GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
 | GTacWth _ -> false
 
 let is_rec_rhs = function
 | GTacFun _ -> true
 | GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _
-| GTacSet _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _
+| GTacSet _ | GTacExt _ | GTacPrm _ | GTacCst _
 | GTacCse _ | GTacOpn _ | GTacWth _ -> false
 
 let rec fv_type f t accu = match t with
@@ -1294,8 +1294,6 @@ let rec subst_expr subst e = match e with
 | GTacLet (r, bs, e) ->
   let bs = List.map (fun (na, e) -> (na, subst_expr subst e)) bs in
   GTacLet (r, bs, subst_expr subst e)
-| GTacArr el ->
-  GTacArr (List.map (fun e -> subst_expr subst e) el)
 | GTacCst (t, n, el) as e0 ->
   let t' = subst_or_tuple subst_kn subst t in
   let el' = List.smartmap (fun e -> subst_expr subst e) el in
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 ->
diff --git a/src/tac2print.ml b/src/tac2print.ml
index e3095c7a89..29f78f251e 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -177,8 +177,6 @@ let pr_glbexpr_gen lvl c =
     | E2 | E3 | E4 | E5 -> fun x -> x
     in
     paren (prlist_with_sep (fun () -> str "," ++ spc ()) (pr_glbexpr E1) cl)
-  | GTacArr cl ->
-    mt () (** FIXME when implemented *)
   | GTacCst (Other tpe, n, cl) ->
     begin match Tac2env.interp_type tpe with
     | _, GTydAlg { galg_constructors = def } ->