From 1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:34:09 +0000
Subject: 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
---
 plugins/quote/quote.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 0cf4d3bb49..80053ea4d0 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
-- 
cgit v1.2.3