Proofview.Goal.sigma returns an indexed evarmap.

1 files changed, 8 insertions, 8 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4e4eafe4e..4a520612f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -76,7 +76,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   (** [clenv] has been generated by a hint-making function, so the only relevant
       data in its evarmap is the set of metas. The [evar_reset_evd] function
       below just replaces the metas of sigma by those coming from the clenv. *)
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (** Still, we need to update the universes *)
   let clenv, c =
@@ -153,7 +153,7 @@ let conclPattern concl pat tac =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
      let env = Proofview.Goal.env gl in
-     let sigma = Proofview.Goal.sigma gl in
+     let sigma = Tacmach.New.project gl in
        constr_bindings env sigma >>= fun constr_bindings ->
      Hook.get forward_interp_tactic constr_bindings tac
   end }
@@ -322,7 +322,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   let intro_tac =
     Tacticals.New.tclTHEN (dbg_intro dbg)
       ( Proofview.Goal.enter { enter = begin fun gl ->
-          let sigma = Proofview.Goal.sigma gl in
+          let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
@@ -417,7 +417,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
 let trivial ?(debug=Off) lems dbnames =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
   let d = mk_trivial_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
@@ -428,7 +428,7 @@ let trivial ?(debug=Off) lems dbnames =
 let full_trivial ?(debug=Off) lems =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
   let d = mk_trivial_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
@@ -459,7 +459,7 @@ let possible_resolve dbg mod_delta db_list local_db cl =
 
 let extend_local_db decl db gl =
   let env = Tacmach.New.pf_env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db
 
 (* Introduce an hypothesis, then call the continuation tactic [kont]
@@ -500,7 +500,7 @@ let default_search_depth = ref 5
 let delta_auto debug mod_delta n lems dbnames =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
   let d = mk_auto_dbg debug in
   let hints = make_local_hint_db env sigma false lems in
@@ -523,7 +523,7 @@ let default_auto = auto !default_search_depth [] []
 let delta_full_auto ?(debug=Off) mod_delta n lems =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
   let d = mk_auto_dbg debug in
   let hints = make_local_hint_db env sigma false lems in