diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /plugins/quote/quote.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'plugins/quote/quote.ml')
-rw-r--r-- | plugins/quote/quote.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ff6acf13..b3ea4335 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -101,7 +101,7 @@ (*i*) -open Errors +open CErrors open Util open Names open Term @@ -109,6 +109,7 @@ open Pattern open Patternops open Constr_matching open Tacmach +open Proofview.Notations (*i*) (*s First, we need to access some Coq constants @@ -227,7 +228,7 @@ let compute_ivs f cs gl = let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let is_conv = Reductionops.is_conv env sigma in begin match decomp_term body3 with | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) @@ -446,7 +447,7 @@ let quote_terms ivs lc = yet. *) let quote f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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 let ivs = compute_ivs f cl gl in @@ -459,10 +460,10 @@ let quote f lid = match ivs.variable_lhs with | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end + end } let gen_quote cont c f lid = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { 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 let ivs = compute_ivs f cl gl in @@ -474,7 +475,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 + end } (*i |