From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 20 Nov 2016 22:16:08 +0100
Subject: Proofview.Goal primitive now return EConstrs.

---
 plugins/quote/quote.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 04a747fb4..5f8a0b2d5 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -452,6 +452,7 @@ let quote f lid =
     let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     let ivs = compute_ivs f cl gl in
     let concl = Proofview.Goal.concl gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let quoted_terms = quote_terms ivs [concl] in
     let (p, vm) = match quoted_terms with
       | [p], vm -> (p,vm)
-- 
cgit v1.2.3