2 files changed, 3 insertions, 2 deletions
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fd87d5b7d3..e7e6ecef98 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,7 +13,8 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
-open Constrarg
+open Stdarg
+open Tacarg
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index b3ea4335f6..6405c8cebd 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -183,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