3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 35178aa1e..8c15f54af 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let identity = Universes.constr_of_global (Lazy.force _I) in
     (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in 
     let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 8d60b8ba2..04936cd83 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -228,7 +228,7 @@ let compute_ivs f cs gl =
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
         let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let is_conv = Reductionops.is_conv env sigma in
           begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 8ff4230e8..dbe7710eb 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -749,7 +749,7 @@ let ltac_ring_structure e =
 
 let ring_lookup (f:glob_tactic_expr) lH rl t =
   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
     try (* find_ring_strucure can raise an exception *)
       let evdref = ref sigma in
@@ -1021,7 +1021,7 @@ let ltac_field_structure e =
 
 let field_lookup (f:glob_tactic_expr) lH rl t =
   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
     try
       let evdref = ref sigma in