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/lemmas.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'vernac/lemmas.ml') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 22f0d199c..be9de5b30 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -14,6 +14,7 @@ open Util open Pp open Names open Term +open Constr open Declarations open Declareops open Entries @@ -62,7 +63,7 @@ let adjust_guardness_conditions const = function { const with const_entry_body = Future.chain const.const_entry_body (fun ((body, ctx), eff) -> - match kind_of_term body with + match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = List.map2 (fun i c -> match i with Some i -> i | None -> @@ -97,7 +98,7 @@ let find_mutually_recursive_statements thms = let ind_hyps = List.flatten (List.map_i (fun i decl -> let t = RelDecl.get_type decl in - match kind_of_term t with + match Constr.kind t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Decl_kinds.CoFinite -> @@ -107,7 +108,7 @@ let find_mutually_recursive_statements thms = let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in - match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with + match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> @@ -246,7 +247,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let rec body_i t = match kind_of_term t with + let rec body_i t = match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) -- cgit v1.2.3