[proof] Attempt to deprecate some V82 parts of the proof API.

I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.

However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.

Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cc9d98f6f..62f3866de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       invEnv ~init:Context.Named.empty
   end in
   let avoid = ref Id.Set.empty in
-  let { sigma=sigma } = Proof.V82.subgoals pf in
+  let _,_,_,_,sigma = Proof.proof pf in
   let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
     match EConstr.kind sigma c with