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

3 files changed, 63 insertions, 37 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index dee57cd04f..0d12388146 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -246,7 +246,8 @@ let build_projection intype outtype (cstr:constructor) special default gls=
 let _M =mkMeta
 
 let rec proof_tac p : unit Proofview.tactic =
-  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
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> Proofview.V82.tactic (exact_check c)
@@ -281,7 +282,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	let typf = Termops.refresh_universes (type_of tf1) in
 	let typx = Termops.refresh_universes (type_of tx1) in
 	let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in
-        Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) >>= fun id ->
+        let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
@@ -310,57 +311,72 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let intype = Termops.refresh_universes (type_of ti) in
 	 let outtype = Termops.refresh_universes (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
-         Tacmach.New.of_old (build_projection intype outtype cstr special default) >>= fun proj ->
+         let proj =
+           Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
+         in
 	 let injt=
 	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
 	   Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf)
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let refute_tac c t1 t2 p =
+  Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) >>= fun intype ->
+  let intype =
+    Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) gl
+  in
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
+  let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
     Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
       [proof_tac p; simplest_elim false_t]
+  end
 
 let convert_to_goal_tac c t1 t2 p = 
+  Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) >>= fun sort ->
+  let sort =
+    Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) gl
+  in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) >>= fun e ->
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun x ->
+  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
   let identity=mkLambda (Name x,sort,mkRel 1) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
     Tacticals.New.tclTHENS (assert_tac (Name e) neweq)
       [proof_tac p; Proofview.V82.tactic (exact_check endt)]
+  end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
+  Proofview.Goal.enter begin fun gl ->
   let tt2=constr_of_term t2 in
-  Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>= fun h ->
+  let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
+  end
 
 let discriminate_tac cstr p =
   Proofview.Goal.enter begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-    Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype ->
+    let intype =
+      Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) gl
+    in
     let concl = Proofview.Goal.concl gl in
     let outsort = mkType (Termops.new_univ ()) in
-    Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid ->
-    Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid ->
+    let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in
     let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
-    Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial ->
+    let trivial = Tacmach.New.of_old (fun gls -> pf_type_of gls identity) gl in
     let outtype = mkType (Termops.new_univ ()) in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
-    Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
-    Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj ->
+    let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+    let proj = Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) gl in
     let injt=mkApp (Lazy.force _f_equal,
 		    [|intype;outtype;proj;t1;t2;mkVar hid|]) in
     let endt=mkApp (Lazy.force _eq_rect,
@@ -383,7 +399,7 @@ let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter begin fun gl ->
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (Pp.str "Reading subgoal ...") in
-    Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state ->
+    let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
     let _ = debug (Pp.str "Problem built, solving ...") in
     let sol = execute true state in
     let _ = debug (Pp.str "Computation completed.") in
@@ -457,7 +473,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 let f_equal =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+    let type_of = Tacmach.New.pf_apply Typing.type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         let ty = Termops.refresh_universes (type_of c1) in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c865639e64..a647238bf8 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -35,8 +35,9 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Tacmach.New.pf_global id >>= fun c ->
-  simplest_elim c
+  Proofview.Goal.enter begin fun gl ->
+    simplest_elim (Tacmach.New.pf_global id gl)
+  end
 let resolve_id id gl = apply (pf_global gl id) gl
 
 let timing timer_name f arg = f arg
@@ -1379,10 +1380,10 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.tclUNIT () >= fun () -> (* delay for the effects in [clear_tables] *)
+  Proofview.Goal.enter begin fun gl ->
   clear_tables ();
-  Tacmach.New.pf_hyps_types >>= fun hyps_types ->
-  Tacmach.New.of_old destructure_omega >>= fun destructure_omega ->
+  let hyps_types = Tacmach.New.pf_hyps_types gl in
+  let destructure_omega = Tacmach.New.of_old destructure_omega gl in
   let tactic_normalisation, system =
     List.fold_left destructure_omega ([],[]) hyps_types in
   let prelude,sys =
@@ -1427,11 +1428,13 @@ let coq_omega =
       Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
     with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
   end
+  end
 
 let coq_omega = coq_omega
 
 let nat_inject =
-  Tacmach.New.pf_apply Reductionops.is_conv >>= fun is_conv ->
+  Proofview.Goal.enter begin fun gl ->
+  let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
     try match destructurate_term t with
       | Kapp(Plus,[t1;t2]) ->
@@ -1562,8 +1565,9 @@ let nat_inject =
 	    | _ -> loop lit
 	  with e when catchable_exception e -> loop lit end
   in
-  Tacmach.New.pf_hyps_types >>= fun hyps_types ->
+  let hyps_types = Tacmach.New.pf_hyps_types gl in
   loop (List.rev hyps_types)
+  end
 
 let dec_binop = function
   | Zne -> coq_dec_Zne
@@ -1633,21 +1637,25 @@ let onClearedName id tac =
   (* so renaming may be necessary *)
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (tclTRY (clear [id])))
-    (Tacmach.New.of_old (fresh_id [] id) >>= fun id ->
-     Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id))
+    (Proofview.Goal.enter begin fun gl ->
+     let id = Tacmach.New.of_old (fresh_id [] id) gl in
+     Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
+    end)
 
 let onClearedName2 id tac =
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (tclTRY (clear [id])))
-    (Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) >>= fun id1 ->
-     Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) >>= fun id2 ->
-      Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ])
+    (Proofview.Goal.enter begin fun gl ->
+     let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
+     let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
+      Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ]
+    end)
 
 let destructure_hyps =
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  Tacmach.New.of_old decidability >>= fun decidability ->
-  Tacmach.New.of_old pf_nf >>= fun pf_nf ->
   Proofview.Goal.enter begin fun gl ->
+  let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+  let decidability = Tacmach.New.of_old decidability gl in
+  let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | (i,body,t)::lit ->
@@ -1791,7 +1799,7 @@ let destructure_hyps =
 let destructure_goal =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    Tacmach.New.of_old decidability >>= fun decidability ->
+    let decidability = Tacmach.New.of_old decidability gl in
     let rec loop t =
       match destructurate_prop t with
       | Kapp(Not,[t]) ->
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 89d161f73e..532a2f11d6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -454,8 +454,8 @@ let quote_terms ivs lc =
 
 let quote f lid =
   Proofview.Goal.enter begin fun gl ->
-    Tacmach.New.pf_global f >>= fun f ->
-    Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+    let f = Tacmach.New.pf_global f gl in
+    let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
     let concl = Proofview.Goal.concl gl in
     Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
@@ -469,8 +469,9 @@ let quote f lid =
   end
 
 let gen_quote cont c f lid =
-  Tacmach.New.pf_global f >>= fun f ->
-  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+  Proofview.Goal.enter begin fun gl ->
+  let f = Tacmach.New.pf_global f gl in
+  let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
   Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
   Proofview.Goal.lift (quote_terms ivs [c]) >>= fun quoted_terms ->
   let (p, vm) = match quoted_terms with
@@ -480,6 +481,7 @@ let gen_quote cont c f lid =
   match ivs.variable_lhs with
     | None -> cont (mkApp (f, [| p |]))
     | Some _ -> cont (mkApp (f, [| vm; p |]))
+  end
 
 (*i