From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 plugins/quote/g_quote.ml4         | 14 +++++++-------
 plugins/quote/quote.ml            | 13 +++++++------
 plugins/quote/quote_plugin.mllib  |  3 ---
 plugins/quote/quote_plugin.mlpack |  2 ++
 4 files changed, 16 insertions(+), 16 deletions(-)
 delete mode 100644 plugins/quote/quote_plugin.mllib
 create mode 100644 plugins/quote/quote_plugin.mlpack

(limited to 'plugins/quote')

diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fdc5c2bb..fd87d5b7 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,19 +13,19 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
+open Constrarg
 
 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 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
 
diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
deleted file mode 100644
index d1b3ccbe..00000000
--- 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 00000000..2e9be09d
--- /dev/null
+++ b/plugins/quote/quote_plugin.mlpack
@@ -0,0 +1,2 @@
+Quote
+G_quote
-- 
cgit v1.2.3