More idiomatic evar map handling

This change is not expected to fix bugs but usually at the start of a
Goal.enter we get the evar map with Goal.sigma not by using tclEVARMAP.

src/aac_rewrite.ml

@@ -17,22 +17,19 @@ module Control =   struct
 end
 
 module Debug = Helper.Debug (Control)
-open Debug
 
 let time_tac msg tac =
   if Control.time then  Proofview.tclTIME (Some msg) tac else tac
 
 let tclTac_or_exn (tac : 'a Proofview.tactic) exn msg : 'a Proofview.tactic =
   Proofview.tclORELSE tac
     (fun e ->
-      let open Proofview.Notations in
       let open Proofview in
-      tclEVARMAP >>= fun sigma ->
       Goal.enter_one (fun gl ->
-          let env = Proofview.Goal.env gl in
-          pr_constr env sigma "last goal" (Goal.concl gl);
-          exn msg e)
-    )
+          let env = Goal.env gl in
+          let sigma = Goal.sigma gl in
+          Debug.pr_constr env sigma "last goal" (Goal.concl gl);
+          exn msg e))
 
 
 open EConstr
@@ -188,7 +185,7 @@ let aac_conclude env sigma (concl:types): ( Evd.evar_map * constr * aac_lift * T
       let eq = Coq.Equivalence.to_relation lift.e in
       let tleft,tright, sigma = Theory.Trans.t_of_constr env sigma eq envs (left,right) in
       let sigma, ir = Theory.Trans.ir_of_envs env sigma eq envs in
-      let _ = pr_constr env sigma "concl" concl in
+      let () = Debug.pr_constr env sigma "concl" concl in
       (sigma,left,lift,ir,tleft,tright)
   with
   | Not_found -> Coq.user_error @@ Pp.strbrk "No lifting from the goal's relation to an equivalence"
@@ -199,12 +196,11 @@ let aac_normalise =
   let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in
   let norm_tac = KerName.make mp (Label.make "internal_normalize") in
   let norm_tac = Locus.ArgArg (None, norm_tac) in
-  let open Proofview.Notations in
   let open Proofview in
   Proofview.Goal.enter (fun goal -> 
       let ids = Tacmach.pf_ids_of_hyps goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let concl = Proofview.Goal.concl goal in
       let sigma,left,lift,ir,tleft,tright = aac_conclude env sigma concl in
       Tacticals.tclTHENLIST
@@ -240,13 +236,11 @@ let aac_reflexivity : unit Proofview.tactic =
 
 (** A sub-tactic to lift the rewriting using Lift  *)
 let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): unit Proofview.tactic =
-  let open Proofview.Notations in
-  let open Proofview in
   Proofview.Goal.enter (fun goal ->
       (* catch the equation and the two members*)
       let concl = Proofview.Goal.concl goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let (left, right, _ ) = match  Coq.match_as_equation env sigma concl with
         | Some x -> x
         | None -> Coq.user_error @@ Pp.strbrk "The goal is not an equation"
@@ -282,11 +276,10 @@ let core_aac_rewrite ?abort
       subst
       (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> unit Proofview.tactic)
       (tr : constr) t left : unit Proofview.tactic =
-  let open Proofview.Notations in
   Proofview.Goal.enter (fun goal ->
       let env = Proofview.Goal.env goal in
-      Proofview.tclEVARMAP >>= fun sigma ->
-      pr_constr env sigma "transitivity through" tr;
+      let sigma = Proofview.Goal.sigma goal in
+      Debug.pr_constr env sigma "transitivity through" tr;
       let tran_tac =
         lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt
       in
@@ -328,13 +321,11 @@ let choose_subst  subterm sol m=
 (** rewrite the constr modulo AC from left to right in the left member
     of the goal *)
 let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ?extra ~occ_subterm ~occ_sol rew : unit Proofview.tactic =
-  let open Proofview.Notations in
-  let open Proofview in
   Proofview.Goal.enter (fun goal ->
       let envs = Theory.Trans.empty_envs () in
       let (concl : types) = Proofview.Goal.concl goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let (_,_,rlt) as concl =
         match Coq.match_as_equation env sigma concl with
         | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation"

src/theory.ml

@@ -990,12 +990,11 @@ module Trans = struct
       able to build the sigmas *)
   let build_sigma_maps (rlt : Coq.Relation.t) zero ir : (sigmas * sigma_maps) Proofview.tactic =
     let open Proofview.Notations in
-    let open Proofview in
-    tclEVARMAP >>= fun sigma ->
     Proofview.Goal.enter_one (fun goal ->
         let env = Proofview.Goal.env goal in
+        let sigma = Proofview.Goal.sigma goal in
         let sigma,rp = build_reif_params env sigma rlt zero in
-        Unsafe.tclEVARS sigma
+        Proofview.Unsafe.tclEVARS sigma
         <*> let renumbered_sym, to_local, to_global = renumber ir.sym  in
             let env_sym = Sigma.of_list
                             rp.sym_ty
@@ -1034,7 +1033,7 @@ module Trans = struct
 	        units_to_pos = (let units = f units in fun x ->  (List.assoc  x units));
               }
             in
-            tclUNIT (sigmas, sigma_maps))
+            Proofview.tclUNIT (sigmas, sigma_maps))
 
   (** builders for the reification *)
   type reif_builders =