Removing various tactic compatibility layers in core tactics.

3 files changed, 24 insertions, 17 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364f..42230dff17 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
-    | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+    | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
     | Unfold_nth c ->
-      Proofview.V82.tactic (fun gl ->
-       if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
-       else tclFAIL 0 (str"Unbound reference") gl)
+      Proofview.Goal.enter { enter = begin fun gl ->
+       if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+       else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+       end }
     | Extern tacast -> 
       conclPattern concl p tacast
   in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d70275dee5..54e4405d1c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,18 +221,22 @@ let auto_unif_flags freeze st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+  let open Tacmach.New in
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = project gl in
   let (c, _, _) = c in
-  let c, gl =
+  let c, sigma =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-        c, {gl with sigma = evd}
-    else c, gl
+        c, evd
+    else c, sigma
   in
-  let t1 = pf_unsafe_type_of gl c in
-  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+  let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+  Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+  end }
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -455,7 +459,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+             e_give_exact flags poly (c,clenv)
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
@@ -1613,9 +1617,11 @@ let not_evar c =
   | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
   | _ -> Proofview.tclUNIT ()
 
-let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
-  else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+  let open Tacticals.New in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evarutil.is_ground_term sigma c then tclIDTAC
+  else tclFAIL 0 (str"Not ground")
 
 let autoapply c i =
   let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972f..738cc0feba 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
 val not_evar : constr -> unit Proofview.tactic
 
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
 
 val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic