From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 engine/proofview.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..ecea637947 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1104,13 +1104,6 @@ module Goal = struct
         tclZERO ~info e
     end
     end
-
-  let normalize { self; state } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
   let gmake env sigma goal =
     let state = get_state goal in
     let goal = drop_state goal in
-- 
cgit v1.2.3


From 3c6ed7485293c7eb80f9c4d415af0ee0b977f157 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 3 May 2019 00:41:55 +0200
Subject: Generalize map_named_val to handle whole declarations.

---
 engine/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..6992d15fcb 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
   let apply_subst_einfo _ ei =
     Evd.({ ei with
        evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps;
        evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
-- 
cgit v1.2.3


From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Nov 2018 23:26:06 +0100
Subject: Moving Evd.evars_of_term from constr to econstr + consequences.

This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
---
 engine/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index ecea637947..b77839c28e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1253,7 +1253,7 @@ module V82 = struct
 
   let top_evars initial =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+      Evar.Set.elements (Evd.evars_of_term c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
-- 
cgit v1.2.3


From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Nov 2018 00:17:47 +0100
Subject: Passing evar_map to evars_of_term rather than expecting the term to
 be evar-nf.

---
 engine/proofview.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index b77839c28e..1fd8b5d50e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -641,7 +641,7 @@ let shelve_goals l =
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
 
 let unifiable_delayed g l =
   CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
@@ -1251,9 +1251,9 @@ module V82 = struct
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
-  let top_evars initial =
+  let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
+      Evar.Set.elements (Evd.evars_of_term sigma c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
-- 
cgit v1.2.3