Proofview.Goal.sigma returns an indexed evarmap.

1 files changed, 40 insertions, 40 deletions

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 ->