Skip to content

Commit

Permalink
Replace an Obj.magic with an Unsafe.tclEVARS
Browse files Browse the repository at this point in the history
mattam82 committed Dec 21, 2017
1 parent cf6feca commit 1f74f84
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/splitting.ml
Original file line number Diff line number Diff line change
@@ -167,9 +167,8 @@ let term_of_tree status isevar env0 tree =
let evm, term, ty = aux env evm x in
(evm, applistc term args) end) rest)
in
let pv : Proofview_monad.proofview = Obj.magic pv in
let pv = { pv with Proofview_monad.solution = evm } in
let _, pv', _, _ = Proofview.apply env tac (Obj.magic pv) in
let tac = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) tac in
let _, pv', _, _ = Proofview.apply env tac pv in
let c = List.hd (Proofview.partial_proof entry pv') in
Proofview.return pv',
it_mkLambda_or_LetIn (subst_vars substc c) ctx, it_mkProd_or_LetIn ty ctx

0 comments on commit 1f74f84

Please sign in to comment.