Getting rid of Goal.here, and all the related exceptions and combinators.

It was a bad idea. The new API based on lists seems more sensible.

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

5 files changed, 21 insertions, 19 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 46a7e596c..4585468ad 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,7 +217,7 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Goal.concl >>- fun concl ->
+    Proofview.Goal.concl >>- fun concl ->
     let eq = Lazy.force eq in
     let t = decomp_term concl in
     match t with
@@ -230,7 +230,7 @@ module Btauto = struct
       Tacticals.New.tclFAIL 0 msg
 
   let tac =
-    Goal.concl >>- fun concl ->
+    Proofview.Goal.concl >>- fun concl ->
     let eq = Lazy.force eq in
     let bool = Lazy.force Bool.typ in
     let t = decomp_term concl in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 63b6375e1..e120de478 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -348,7 +348,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
 let discriminate_tac cstr p =
   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 ->
-  Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>- fun concl ->
   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 ->
@@ -394,7 +394,7 @@ let cc_tactic depth additionnal_terms =
 		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 		discriminate_tac cstr p
 	    | Incomplete ->
-                Goal.env >>- fun env ->
+                Proofview.Goal.env >>- fun env ->
 		let metacnt = ref 0 in
 		let newmeta _ = incr metacnt; _M !metacnt in
 		let terms_to_complete =
@@ -451,7 +451,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 *)
 
 let f_equal =
-  Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>- fun concl ->
   Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
   let cut_eq c1 c2 =
     let ty = Termops.refresh_universes (type_of c1) in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 512e372bb..adc1d9ee3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1781,11 +1781,11 @@ let destructure_hyps =
 	  | e when catchable_exception e -> loop lit
 	end
   in
-  Goal.hyps >>- fun hyps ->
+  Proofview.Goal.hyps >>- fun hyps ->
   loop (Environ.named_context_of_val hyps)
 
 let destructure_goal =
-  Goal.concl >>- fun concl ->
+  Proofview.Goal.concl >>- fun concl ->
   Tacmach.New.of_old decidability >>- fun decidability ->
   let rec loop t =
     match destructurate_prop t with
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 0cf4d3bb4..80053ea4d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -227,7 +227,9 @@ let compute_ivs f cs =
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
-	Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv ->
+        Goal.env >- fun env ->
+        Goal.defs >- fun sigma ->
+        let is_conv = Reductionops.is_conv env sigma in
         Goal.return
           begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
@@ -452,10 +454,10 @@ let quote_terms ivs lc =
 
 let quote f lid =
   Tacmach.New.pf_global f >>- fun f ->
-  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
-  compute_ivs f cl >>- fun ivs ->
-  Goal.concl >>- fun concl ->
-  quote_terms ivs [concl] >>- fun quoted_terms ->
+  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
+  Proofview.Goal.lift (compute_ivs f cl) >>- fun ivs ->
+  Proofview.Goal.concl >>- fun concl ->
+  Proofview.Goal.lift (quote_terms ivs [concl]) >>- fun quoted_terms ->
   let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false
@@ -466,9 +468,9 @@ let quote f lid =
 
 let gen_quote cont c f lid =
   Tacmach.New.pf_global f >>- fun f ->
-  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
-  compute_ivs f cl >>- fun ivs ->
-  quote_terms ivs [c] >>- fun quoted_terms ->
+  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>- fun cl ->
+  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
     | [p], vm -> (p,vm)
     | _ -> assert false
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 907cd474c..011aba5d7 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -798,8 +798,8 @@ let ltac_ring_structure e =
 open Proofview.Notations
 
 let ring_lookup (f:glob_tactic_expr) lH rl t =
-  Goal.env >>- fun env ->
-  Goal.defs >>- fun sigma ->
+  Proofview.tclEVARMAP >= fun sigma ->
+  Proofview.Goal.env >>- fun env ->
   let rl = make_args_list rl t in
   let e = find_ring_structure env sigma rl in
   let rl = carg (make_term_list e.ring_carrier rl) in
@@ -1119,8 +1119,8 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f:glob_tactic_expr) lH rl t =
-  Goal.env >>- fun env ->
-  Goal.defs >>- fun sigma ->
+  Proofview.tclEVARMAP >= fun sigma ->
+  Proofview.Goal.env >>- fun env ->
   let rl = make_args_list rl t in
   let e = find_field_structure env sigma rl in
   let rl = carg (make_term_list e.field_carrier rl) in