2 files changed, 14 insertions, 7 deletions
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg
index c35e0fe1..749903c3 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.mlg
@@ -8,32 +8,39 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Ltac_plugin
 open Names
-open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
 open Stdarg
 open Tacarg
 
+}
+
 DECLARE PLUGIN "quote_plugin"
 
+{
+
 let cont = Id.of_string "cont"
 let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in
+  let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make 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.tag tac))
 
+}
+
 TACTIC EXTEND quote
-  [ "quote" ident(f) ] -> [ quote f [] ]
-| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+| [ "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 [] ]
+  { 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 ]
+  { gen_quote (make_cont k) c f lc }
 END
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 912429c3..7464b42d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -120,7 +120,7 @@ open Proofview.Notations
   the constants are loaded in the environment *)
 
 let constant dir s =
-  EConstr.of_constr @@ Universes.constr_of_global @@
+  EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "Quote" ("quote"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")