Add a more general quote construction

"quote f [...] in c using t" will call t (must be an ltac function)
with a X (of form "f x" or "f vm x") such that X converts to c. In
particular,

  match goal with
    | H : ?x |- _ =>
      quote f in x using (fun X => change X in H)
  end

may be used as an equivalent of plain quote that acts on an
hypothesis. The construction can be used in a more general way,
though.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12037 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 2 deletions

diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 808cbbf27..bdeb9844b 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -10,9 +10,22 @@
 
 (* $Id$ *)
 
+open Util
+open Tacexpr
 open Quote
 
+let make_cont k x =
+  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst k)) in
+  let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
+  let tac = <:tactic<let cont := $k in cont $x>> in
+  Tacinterp.interp tac
+
 TACTIC EXTEND quote
   [ "quote" ident(f) ] -> [ quote f [] ]
 | [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] ->
+  [ gen_quote (make_cont k) c f [] ]
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"
+    "in" constr(c) "using" tactic(k) ] ->
+  [ gen_quote (make_cont k) c f lc ]
 END
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index c2193fb48..16cc3a731 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -438,8 +438,8 @@ let quote_terms ivs lc gl =
   (lp, (btree_of_array (Array.of_list (List.rev !varlist))
           ivs.return_type ))
 
-(*s actually we could "quote" a list of terms instead of the conclusion of
-  current goal. Ring for example needs that, but Ring doesn't use Quote
+(*s actually we could "quote" a list of terms instead of a single
+  term. Ring for example needs that, but Ring doesn't use Quote
   yet. *)
 
 let quote f lid gl =
@@ -454,6 +454,18 @@ let quote f lid gl =
     | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
     | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
 
+let gen_quote cont c f lid gl =
+  let f = pf_global gl f in
+  let cl = List.map (pf_global gl) lid in
+  let ivs = compute_ivs gl f cl in
+  let (p, vm) = match quote_terms ivs [c] gl with
+    | [p], vm -> (p,vm)
+    | _ -> assert false
+  in
+  match ivs.variable_lhs with
+    | None -> cont (mkApp (f, [| p |])) gl
+    | Some _ -> cont (mkApp (f, [| vm; p |])) gl
+
 (*i
 
 Just testing ...