From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

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

(limited to 'plugins/derive/derive.ml')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52..f23f4ce7d 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -37,6 +37,7 @@ let start_deriving f suchthat lemma =
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
         let evdref = ref sigma in
         let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
+        let suchthat = EConstr.Unsafe.to_constr suchthat in
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
-- 
cgit v1.2.3