1 files changed, 49 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b8f065b41..d08dfd67d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -203,3 +203,52 @@ let pr_glls glls =
   hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
          prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
 
+(* Variants of [Tacmach] functions built with the new proof engine *)
+module New = struct
+  open Proofview.Notations
+
+  let pf_apply f =
+    Goal.env >- fun env ->
+    Goal.defs >- fun sigma ->
+    Goal.return (f env sigma)
+
+  let of_old f =
+    Goal.V82.to_sensitive f
+
+  let pf_global id =
+    Goal.hyps >- fun hyps ->
+    let hyps = Environ.named_context_of_val hyps in
+    Goal.return (Constrintern.construct_reference hyps id)
+
+  let pf_ids_of_hyps =
+    Goal.hyps >- fun hyps ->
+      let hyps = Environ.named_context_of_val hyps in
+      Goal.return (ids_of_named_context hyps)
+
+  let pf_get_new_id id =
+    pf_ids_of_hyps >- fun ids ->
+    Goal.return (next_ident_away id ids)
+
+  let pf_get_hyp id =
+    Goal.hyps >- fun hyps ->
+    let hyps = Environ.named_context_of_val hyps in
+    let sign =
+      try Context.lookup_named id hyps
+      with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
+    in
+    Goal.return sign
+
+  let pf_get_hyp_typ id =
+    pf_get_hyp id >- fun (_,_,ty) ->
+    Goal.return ty
+
+  let pf_hyps_types =
+    Goal.env >- fun env ->
+    let sign = Environ.named_context env in
+    Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+
+  let pf_last_hyp =
+    Goal.hyps >- fun hyps ->
+    Goal.return (List.hd (Environ.named_context_of_val hyps))
+
+end