From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 13:04:45 +0200 Subject: Boxing the Goal.enter primitive into a record type. --- plugins/quote/quote.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2a2ef30fb1..8d60b8ba2a 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -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 @@ -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 -- cgit v1.2.3 From 2d747797c427818cdf85d0a0d701c7c9b0106b82 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 16:12:39 +0200 Subject: Proofview.Goal.sigma returns an indexed evarmap. --- plugins/quote/quote.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 8d60b8ba2a..04936cd835 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -228,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) -> (*

Case c of c1 ... cn end *) -- cgit v1.2.3 From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 19 Nov 2015 17:48:32 +0100 Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. --- plugins/quote/quote.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2a2ef30fb1..b72ebbc927 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c in aux bodyi -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/quote/Quote.v | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/quote/quote.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index ca1a18e802..2d154adc57 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ quote f [] ] -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- plugins/quote/g_quote.ml4 | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins/quote') diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 7a3d7936a6..a15b0eb05a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,6 +13,10 @@ open Misctypes open Tacexpr open Geninterp open Quote +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "quote_plugin" -- cgit v1.2.3