From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- stm/lemmas.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 55f33be39..9896d5a93 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -108,7 +108,7 @@ let find_mutually_recursive_statements thms = (* Cofixpoint or fixpoint w/o explicit decreasing argument *) | None | Some (None, CStructRec) -> let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_all_stack env Evd.empty c)) + (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c)))) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> @@ -122,8 +122,8 @@ let find_mutually_recursive_statements thms = []) 0 (List.rev whnf_hyp_hds)) in let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in - match kind_of_term whnf_ccl with + 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 | 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 -> -- cgit v1.2.3