aboutsummaryrefslogtreecommitdiff
path: root/plugins/quote
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/quote')
-rw-r--r--plugins/quote/Quote.v2
-rw-r--r--plugins/quote/g_quote.ml417
-rw-r--r--plugins/quote/quote.ml21
-rw-r--r--plugins/quote/quote_plugin.mllib3
-rw-r--r--plugins/quote/quote_plugin.mlpack2
5 files changed, 23 insertions, 22 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e27fe7f454..e7e6ecef98 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,19 +13,20 @@ open Misctypes
open Tacexpr
open Geninterp
open Quote
+open Stdarg
+open Tacarg
DECLARE PLUGIN "quote_plugin"
let loc = Loc.ghost
-let cont = (loc, Id.of_string "cont")
-let x = (loc, Id.of_string "x")
+let cont = Id.of_string "cont"
+let x = Id.of_string "x"
-let make_cont (k : glob_tactic_expr) (c : Constr.t) =
+let make_cont (k : Val.t) (c : Constr.t) =
let c = Tacinterp.Value.of_constr c in
- let tac = TacCall (loc, ArgVar cont, [Reference (ArgVar x)]) in
- let tac = TacLetIn (false, [(cont, Tacexp k)], TacArg (loc, tac)) in
- let ist = { lfun = Id.Map.singleton (snd x) c; extra = TacStore.empty; } in
- Tacinterp.eval_tactic_ist ist tac
+ let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
+ let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
+ Tacinterp.eval_tactic_ist ist (TacArg (loc, tac))
TACTIC EXTEND quote
[ "quote" ident(f) ] -> [ quote f [] ]
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28d5..6405c8cebd 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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
@@ -182,7 +183,7 @@ type inversion_scheme = {
let i_can't_do_that () = error "Quote: not a simple fixpoint"
-let decomp_term c = kind_of_term (strip_outer_cast c)
+let decomp_term c = kind_of_term (Termops.strip_outer_cast c)
(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ...
?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
@@ -211,9 +212,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 (snd (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
- | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+ | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c
in
aux bodyi
@@ -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
diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
deleted file mode 100644
index d1b3ccbe1e..0000000000
--- a/plugins/quote/quote_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Quote
-G_quote
-Quote_plugin_mod
diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack
new file mode 100644
index 0000000000..2e9be09d8d
--- /dev/null
+++ b/plugins/quote/quote_plugin.mlpack
@@ -0,0 +1,2 @@
+Quote
+G_quote
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:35:00 +0000