diff options
| -rw-r--r-- | src/tac2env.ml | 2 | ||||
| -rw-r--r-- | src/tac2expr.mli | 1 | ||||
| -rw-r--r-- | src/tac2intern.ml | 6 | ||||
| -rw-r--r-- | src/tac2interp.ml | 3 | ||||
| -rw-r--r-- | src/tac2print.ml | 2 |
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 } -> |