diff options
| author | aspiwack | 2013-11-02 15:34:09 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:34:09 +0000 |
| commit | 1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 (patch) | |
| tree | 977ac085e6b783933d316b3ff4eef1fba3d4dda9 /plugins/quote | |
| parent | fed5cbc5b006447bb3d877b3eeb35f7c76e96661 (diff) | |
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
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 18 |
1 files changed, 10 insertions, 8 deletions
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 |