diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-01 20:53:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:21:51 +0100 |
| commit | 8f6aab1f4d6d60842422abc5217daac806eb0897 (patch) | |
| tree | c36f2f963064f51fe1652714f4d91677d555727b /stm | |
| parent | 5143129baac805d3a49ac3ee9f3344c7a447634f (diff) | |
Reductionops API using EConstr.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 -> |