Tachmach.New is now in Proofview.Goal.enter style.

As a result the use of the glist-style interface for manipulating goals has almost been removed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 2 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index bc756eb82..c3d83b394 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -351,7 +351,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Tacmach.New.of_old (fun gl -> pf_type_of gl p) >>= fun type_of_pq ->
+  Proofview.Goal.enter begin fun gl ->
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -380,6 +381,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
            Tacticals.New.tclTHENLIST [
              Proofview.V82.tactic (Tactics.emit_side_effects eff);
              Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
+  end
 
 (* used in the bool -> leib side *)
 let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
@@ -410,7 +412,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
   let rec aux l1 l2 =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
-        Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+        Proofview.Goal.enter begin fun gl ->
+        let type_of = Tacmach.New.pf_apply Typing.type_of gl in
         begin try (* type_of can raise an exception *)
         let tt1 = type_of t1 in
         if eq_constr t1 t2 then aux q1 q2
@@ -454,6 +457,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
         )
           with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
         end
+        end
     | ([],[]) -> Proofview.tclUNIT ()
     | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
   in