From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- vernac/obligations.ml | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 785c842ba..e23146273 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -13,6 +13,7 @@ open Declare *) open Term +open Constr open Vars open Names open Evd @@ -55,7 +56,7 @@ let subst_evar_constr evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match kind_of_term c with + let rec substrec (depth, fixrels) c = match Constr.kind c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -85,15 +86,15 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match kind_of_term x with + (fun x -> match Constr.kind x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; mkApp (idf idstr, Array.of_list args) | Fix _ -> - map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c + Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in t', !seen, !transparent @@ -103,9 +104,9 @@ let subst_evar_constr evs n idf t = where n binders were passed through. *) let subst_vars acc n t = let var_index id = Util.List.index Id.equal id acc in - let rec substrec depth c = match kind_of_term c with + let rec substrec depth c = match Constr.kind c with | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> map_constr_with_binders succ substrec depth c + | _ -> Constr.map_with_binders succ substrec depth c in substrec 0 t @@ -144,7 +145,7 @@ let rec chop_product n t = let pop t = Vars.lift (-1) t in if Int.equal n 0 then Some t else - match kind_of_term t with + match Constr.kind t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None @@ -273,7 +274,7 @@ let explain_no_obligations = function | None -> str "No obligations remaining" type obligation_info = - (Names.Id.t * Term.types * Evar_kinds.t Loc.located * + (Names.Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array @@ -384,7 +385,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with + match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -400,13 +401,13 @@ let replace_appvars subst = let f, l = decompose_app c in if isVar f then try - let c' = List.map (map_constr aux) l in + let c' = List.map (Constr.map aux) l in let (t, b) = Id.List.assoc (destVar f) subst in mkApp (delayed_force hide_obligation, [| prod_applist t c'; applistc b c' |]) - with Not_found -> map_constr aux c - else map_constr aux c - in map_constr aux + with Not_found -> Constr.map aux c + else Constr.map aux c + in Constr.map aux let subst_prog expand obls ints prg = let subst = obl_substitution expand obls ints in @@ -490,7 +491,7 @@ let declare_definition prg = cst let rec lam_index n t acc = - match kind_of_term t with + match Constr.kind t with | Lambda (Name n', _, _) when Id.equal n n' -> acc | Lambda (_, _, b) -> @@ -566,9 +567,9 @@ let declare_mutual_definition l = let decompose_lam_prod c ty = let open Context.Rel.Declaration in let rec aux ctx c ty = - match kind_of_term c, kind_of_term ty with + match Constr.kind c, Constr.kind ty with | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when eq_constr b b' && eq_constr t t' -> + when Constr.equal b b' && Constr.equal t t' -> let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in aux ctx' c ty | _, LetIn (x', b', t', ty) -> -- cgit v1.2.3