Proofview.Goal.sigma returns an indexed evarmap.

10 files changed, 98 insertions, 98 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
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 34886d74d..0cc74ff44 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let filter_hyp f tac =
 
 let contradiction_context =
   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 rec seek_neg l = match l with
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
@@ -91,7 +91,7 @@ let is_negation_of env sigma typ t =
 
 let contradiction_term (c,lbind as cl) =
   Proofview.Goal.nf_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 type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 08502e0cc..dbdfb3e92 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -154,8 +154,8 @@ let e_exact poly flags (c,clenv) =
 let rec e_trivial_fail_db db_list local_db =
   let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let d = Tacmach.New.pf_last_hyp gl in
-    let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in
-    e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) hintl local_db)
+    let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
+    e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
   end } in
   Proofview.Goal.enter { enter = begin fun gl ->
   let tacl =
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 27e96637d..d3aa16092 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -97,7 +97,7 @@ let general_decompose recognizer c =
 
 let head_in indl t gl =
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   try
     let ity,_ =
       if !up_to_delta
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0c487c4e6..85bc50216 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -159,7 +159,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let try_occ (evd', c') =
     Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
-  let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in
+  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
     w_unify_to_subterm_all ~flags env eqclause.evd
       ((if l2r then c1 else c2),concl)
@@ -208,7 +208,7 @@ let rewrite_conv_closed_unif_flags = {
 
 let rewrite_elim with_evars frzevars cls c e =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
+  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_conv_closed_unif_flags c in
   general_elim_clause with_evars flags cls c e
   end }
 
@@ -276,7 +276,7 @@ let jmeq_same_dom gl = function
     let rels, t = decompose_prod_assum t in
     let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
     match decompose_app t with
-      | _, [dom1; _; dom2;_] -> is_conv env (Proofview.Goal.sigma gl) dom1 dom2
+      | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
 (* find_elim determines which elimination principle is necessary to
@@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-      let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let sigma, elim = Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c) in
 	sigma, elim, Declareops.no_seff
   else
   let scheme_name = match dep, lft2rgt, inccl with
@@ -337,7 +337,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
       let sigma, elim =
-	Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+	Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c)
       in
 	sigma, elim, eff
   | _ -> assert false
@@ -384,7 +384,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
     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 ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
@@ -484,7 +484,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 
 let apply_special_clear_request clear_flag f =
   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 ((c, bl), sigma) = run_delayed env sigma f in
@@ -496,7 +496,7 @@ let apply_special_clear_request clear_flag f =
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     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 (c, sigma) = run_delayed env sigma f in
       tclWITHHOLES with_evars
@@ -569,9 +569,9 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
   let evd = 
-    if unsafe then Some (Proofview.Goal.sigma gl)
+    if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Proofview.Goal.sigma gl))
+      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -965,7 +965,7 @@ let onEquality with_evars tac (c,lbindc) =
 
 let onNegatedEquality with_evars tac =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match kind_of_term (hnf_constr env sigma ccl) with
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fa13234a6..e1997c705 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -664,7 +664,7 @@ END
 
 let hget_evar n =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
   let evl = evar_list concl in
   if List.length evl < n then
@@ -779,7 +779,7 @@ END
 
 let eq_constr x y = 
   Proofview.Goal.enter { enter = begin fun gl ->
-    let evd = Proofview.Goal.sigma gl in
+    let evd = Tacmach.New.project gl in
       if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () 
       else Tacticals.New.tclFAIL 0 (str "Not equal")
   end }
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2667fa7ff..648d68f27 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1566,7 +1566,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let ty = match clause with
     | None -> concl
     | Some id -> Environ.named_type id env
@@ -2040,7 +2040,7 @@ let not_declared env ty rel =
 let setoid_proof ty fn fallback =
   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 concl = Proofview.Goal.concl gl in
     Proofview.tclORELSE
       begin
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1ea19bce0..da3ab737b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -633,7 +633,7 @@ let pf_interp_constr ist gl =
 let new_interp_constr ist c k =
   let open Proofview in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in
+    let (sigma, c) = interp_constr ist (Goal.env gl) (Tacmach.New.project gl) c in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c)
   end }
 
@@ -790,11 +790,11 @@ let rec message_of_value v =
     Ftactic.return (str "<tactic>")
   else if has_type v (topwit wit_constr) then
     let v = out_gen (topwit wit_constr) v in
-    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end
+    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) v) end
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
     Ftactic.nf_enter begin fun gl ->
-      Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c)
+      Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Tacmach.New.project gl) c)
     end
   else if has_type v (topwit wit_unit) then
     Ftactic.return (str "()")
@@ -804,16 +804,16 @@ let rec message_of_value v =
     let p = out_gen (topwit wit_intro_pattern) v in
     let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in
     Ftactic.nf_enter begin fun gl ->
-      Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p)
+      Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Tacmach.New.project gl) c) p)
     end
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end
+    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) c) end
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
     Ftactic.nf_enter begin fun gl ->
       Ftactic.return (pr_closed_glob_env (pf_env gl)
-                        (Proofview.Goal.sigma gl) c)
+                        (Tacmach.New.project gl) c)
     end
   else match Value.to_list v with
   | Some l ->
@@ -1224,7 +1224,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       | BindingsArgType
       | OptArgType _ | PairArgType _ -> (** generic handler *)
         Ftactic.nf_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 concl = Proofview.Goal.concl gl in
           let goal = Proofview.Goal.goal gl in
@@ -1233,7 +1233,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         end
       | _ as tag -> (** Special treatment. TODO: use generic handler  *)
         Ftactic.nf_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
           match tag with
           | IntOrVarArgType ->
@@ -1352,7 +1352,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       Proofview.Goal.nf_enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
-        let goal_sigma = Proofview.Goal.sigma gl in
+        let goal_sigma = Tacmach.New.project gl in
         let concl = Proofview.Goal.concl gl in
         let goal = Proofview.Goal.goal gl in
         let tac = Tacenv.interp_ml_tactic opn in
@@ -1399,7 +1399,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
   match arg with
   | TacGeneric arg ->
       Ftactic.nf_enter begin fun gl ->
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let goal = Proofview.Goal.goal gl in
         let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
         Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
@@ -1407,7 +1407,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
   | Reference r -> interp_ltac_reference dloc false ist r
   | ConstrMayEval c ->
       Ftactic.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 (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
         Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
@@ -1427,12 +1427,12 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
       interp_app loc ist fv largs
   | TacFreshId l ->
       Ftactic.enter begin fun gl ->
-        let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in
+        let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Tacmach.New.project gl) l in
         Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id)))
       end
   | TacPretype c ->
       Ftactic.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 {closure;term} = interp_uconstr ist env c in
         let vars = {
@@ -1611,7 +1611,7 @@ and interp_match ist lz constr lmr =
     end
   end >>= fun constr ->
   Ftactic.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 ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
     interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr)
@@ -1620,7 +1620,7 @@ and interp_match ist lz constr lmr =
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
     Ftactic.nf_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 hyps = Proofview.Goal.hyps gl in
       let hyps = if lr then List.rev hyps else hyps in
@@ -1767,7 +1767,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
   end >>= fun result ->
   Ftactic.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 result = Value.normalize result in
   try
     let cresult = coerce_to_closed_constr env result in
@@ -1805,7 +1805,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacIntroPattern l ->
       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
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
         Tacticals.New.tclWITHHOLES false 
         (name_atomic ~env
@@ -1817,7 +1817,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacIntroMove (ido,hto) ->
       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
         let mloc = interp_move_location ist env sigma hto in
         let ido = Option.map (interp_ident ist env sigma) ido in
         name_atomic ~env
@@ -1840,7 +1840,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
       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
 	let l = List.map (fun (k,c) ->
           let loc, f = interp_open_constr_with_bindings_loc ist c in
 	    (k,(loc,f))) cb 
@@ -1856,7 +1856,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacElim (ev,(keep,cb),cbo) ->
       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 
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
         let named_tac =
@@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end }
   | TacCase (ev,(keep,cb)) ->
       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 sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let named_tac =
@@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacFix (idopt,n) ->
       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
         let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacFix(idopt,n))
@@ -1905,7 +1905,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacCofix idopt ->
       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
         let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacCofix (idopt))
@@ -1931,7 +1931,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacAssert (b,t,ipat,c) ->
       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
         let (sigma,c) = 
           (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
         in
@@ -1944,7 +1944,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end }
   | TacGeneralize cl ->
       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 sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
         Tacticals.New.tclWITHHOLES false
@@ -1962,7 +1962,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.V82.nf_evar_goals <*>
       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 clp = interp_clause ist env sigma clp in
         let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
         if Locusops.is_nowhere clp then
@@ -2005,7 +2005,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end;
       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
         let lems = interp_auto_lemmas ist env sigma lems in
         name_atomic ~env
           (TacTrivial(debug,List.map snd lems,l))
@@ -2022,7 +2022,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end;
       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
         let lems = interp_auto_lemmas ist env sigma lems in
         name_atomic ~env
           (TacAuto(debug,n,List.map snd lems,l))
@@ -2038,7 +2038,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.V82.nf_evar_goals <*>
       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 sigma,l =
           List.fold_map begin fun sigma (c,(ipato,ipats),cls) ->
             (* TODO: move sigma as a side-effect *)
@@ -2071,7 +2071,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacClear (b,l) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Tacmach.New.pf_env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let l = interp_hyp_list ist env sigma l in
         if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l)
         else
@@ -2082,7 +2082,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacClearBody l ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Tacmach.New.pf_env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let l = interp_hyp_list ist env sigma l in
         name_atomic ~env
           (TacClearBody l)
@@ -2097,7 +2097,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacRename l ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Tacmach.New.pf_env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let l =
           List.map (fun (id1,id2) ->
 	    interp_hyp ist env sigma id1,
@@ -2112,7 +2112,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacSplit (ev,bll) ->
       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
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
         let named_tac =
           let tac = Tactics.split_with_bindings ev bll in
@@ -2165,7 +2165,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.V82.nf_evar_goals <*>
       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
         Proofview.V82.tactic begin fun gl -> 
           let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
@@ -2189,7 +2189,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacSymmetry c ->
       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
         let cl = interp_clause ist env sigma c in
         name_atomic ~env
           (TacSymmetry cl)
@@ -2207,7 +2207,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           } in
 	  (b,m,keep,f)) l in
         let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let cl = interp_clause ist env sigma cl in
         name_atomic ~env
           (TacRewrite (ev,l,cl,by))
@@ -2219,7 +2219,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       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 (sigma,c_interp) =
           match c with
           | None -> sigma , None
@@ -2239,7 +2239,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       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
         let hyps = interp_hyp_list ist env sigma idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
@@ -2251,7 +2251,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInversion (InversionUsing (c,idl),hyp) ->
       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
         let (sigma,c_interp) = interp_constr ist env sigma c in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let hyps = interp_hyp_list ist env sigma idl in
@@ -2413,7 +2413,7 @@ let dummy_id = Id.of_string "_"
 let lift_constr_tac_to_ml_tac vars tac =
   let tac _ ist = 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
     let map = function
     | None -> None
     | Some id ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c67053252..bdbc0aa21 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -696,7 +696,7 @@ module New = struct
   let pf_constr_of_global ref tac =
     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 (sigma, c) = Evd.fresh_global env sigma ref in
       Proofview.Unsafe.tclEVARS sigma <*> (tac c)
     end }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 66053a314..94e334914 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -187,7 +187,7 @@ let introduction ?(check=true) id =
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let hyps = Proofview.Goal.hyps gl in
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
@@ -226,7 +226,7 @@ let convert_concl ?(check=true) ty k =
 let convert_hyp ?(check=true) d =
   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
     let ty = Proofview.Goal.raw_concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
@@ -401,7 +401,7 @@ let find_name mayrepl decl naming gl = match naming with
   | NamingAvoid idl ->
       (* this case must be compatible with [find_intro_names] below. *)
       let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
+      let sigma = Tacmach.New.project gl in
       new_fresh_id idl (default_id env sigma decl) gl
   | NamingBasedOn (id,idl) ->  new_fresh_id idl id gl
   | NamingMustBe (loc,id) ->
@@ -785,7 +785,7 @@ let build_intro_tac id dest tac = match dest with
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
-    let concl = nf_evar (Proofview.Goal.sigma gl) concl in
+    let concl = nf_evar (Tacmach.New.project gl) concl in
     match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
         let name = find_name false (name,None,t) name_flag gl in
@@ -999,7 +999,7 @@ let onOpenInductionArg env sigma tac = function
         (Tacticals.New.onLastHyp
            (fun c ->
              Proofview.Goal.enter { enter = begin fun gl ->
-             let sigma = Proofview.Goal.sigma gl in
+             let sigma = Tacmach.New.project gl in
              let pending = (sigma,sigma) in
              tac clear_flag (pending,(c,NoBindings))
              end }))
@@ -1008,7 +1008,7 @@ let onOpenInductionArg env sigma tac = function
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
         (Proofview.Goal.enter { enter = begin fun gl ->
-         let sigma = Proofview.Goal.sigma gl in
+         let sigma = Tacmach.New.project gl in
          let pending = (sigma,sigma) in
          tac clear_flag (pending,(mkVar id,NoBindings))
         end })
@@ -1038,7 +1038,7 @@ let map_induction_arg f = function
 let cut c =
   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
     let concl = Tacmach.New.pf_nf_concl gl in
     let is_sort =
       try
@@ -1173,7 +1173,7 @@ let enforce_prop_bound_names rename tac =
       let rename_branch i =
         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 t = Proofview.Goal.concl gl in
           change_concl (aux env sigma i t)
         end } in
@@ -1193,7 +1193,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
     rename i (elim, elimty, bindings) indclause =
   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
   let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv =
@@ -1223,7 +1223,7 @@ type eliminator = {
 let general_elim_clause_gen elimtac indclause elim =
   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
   let (elimc,lbindelimc) = elim.elimbody in
   let elimt = Retyping.get_type_of env sigma elimc in
   let i =
@@ -1234,7 +1234,7 @@ let general_elim_clause_gen elimtac indclause elim =
 let general_elim with_evars clear_flag (c, lbindc) elim =
   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
   let ct = Retyping.get_type_of env sigma c in
   let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
@@ -1351,7 +1351,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
     id rename i (elim, elimty, bindings) indclause =
   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
   let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
@@ -1429,7 +1429,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 let descend_in_conjunctions avoid tac (err, info) c =
   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
   try
     let t = Retyping.get_type_of env sigma c in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
@@ -1450,7 +1450,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	  (List.init n (fun i ->
             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
 	    match make_projection env sigma params cstr sign elim i n c u with
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
@@ -1506,7 +1506,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
   let rec try_main_apply with_destruct c =
     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
 
     let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
@@ -1578,7 +1578,7 @@ let rec apply_with_bindings_gen b e = function
 let apply_with_delayed_bindings_gen b e l = 
   let one k (loc, f) =
     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 (cb, sigma) = run_delayed env sigma f in
 	Tacticals.New.tclWITHHOLES e
@@ -1648,7 +1648,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     id (clear_flag,(loc,(d,lbind))) tac =
   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 flags =
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
@@ -1657,7 +1657,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   let rec aux idstoclear with_destruct c =
     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
     try
       let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
       clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1681,7 +1681,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
     id (clear_flag,(loc,f)) tac =
   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
     let (c, sigma) = run_delayed env sigma f in
     Tacticals.New.tclWITHHOLES with_evars 
       (apply_in_once sidecond_first with_delta with_destruct with_evars
@@ -1768,7 +1768,7 @@ let assumption =
     else Tacticals.New.tclZEROMSG (str "No such assumption.")
   | (id, c, t)::rest ->
     let concl = Proofview.Goal.concl gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let (sigma, is_same_type) =
       if only_eq then (sigma, Constr.equal t concl)
       else
@@ -2244,7 +2244,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
         else
           Proofview.V82.tactic (clear [id]) in
       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 (c, sigma) = run_delayed env sigma f in
         Tacticals.New.tclWITHHOLES false
@@ -3677,7 +3677,7 @@ let guess_elim isrec dep s hyp0 gl =
 let given_elim hyp0 (elimc,lbind as e) gl =
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
-  Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
+  Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
     (Id.t list * (elim_arg_kind * bool * Id.t) list) array
@@ -3722,7 +3722,7 @@ let is_functional_induction elimc gl =
 
 let get_eliminator elim dep s gl = match elim with
   | ElimUsing (elim,indsign) ->
-      Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign
+      Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
@@ -4023,7 +4023,7 @@ let induction_gen clear_flag isrec with_evars elim
   | _ -> [] 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
   let ccl = Proofview.Goal.raw_concl gl in
   let cls = Option.default allHypsAndConcl cls in
   let sigma = Sigma.Unsafe.of_evar_map sigma in
@@ -4112,7 +4112,7 @@ let induction_destruct isrec with_evars (lc,elim) =
   | [c,(eqname,names as allnames),cls] ->
     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
     match elim with
     | Some elim when is_functional_induction elim gl ->
       (* Standard induction on non-standard induction schemes *)
@@ -4139,7 +4139,7 @@ let induction_destruct isrec with_evars (lc,elim) =
   | _ ->
     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
     match elim with
     | None ->
       (* Several arguments, without "using" clause *)
@@ -4155,7 +4155,7 @@ let induction_destruct isrec with_evars (lc,elim) =
         (Tacticals.New.tclMAP (fun (a,b,cl) ->
           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      
           onOpenInductionArg env sigma (fun clear_flag a ->
             induction_gen clear_flag false with_evars None (a,b) cl) a
           end }) l)
@@ -4267,7 +4267,7 @@ let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let maybe_betadeltaiota_concl allowred gl =
   let concl = Tacmach.New.pf_nf_concl gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   if not allowred then concl
   else
     let env = Proofview.Goal.env gl in
@@ -4401,7 +4401,7 @@ let prove_transitivity hdcncl eq_kind t =
       mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
   | HeterogenousEq (typ1,c1,typ2,c2) ->
       let env = Proofview.Goal.env gl in
-      let sigma = Proofview.Goal.sigma gl in
+      let sigma = Tacmach.New.project gl in
       let type_of = Typing.unsafe_type_of env sigma in
       let typt = type_of t in
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),