From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

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

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index f88b3a700..981ce2a61 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -312,6 +312,7 @@ let rtauto_tac gls=
 	     str "Giving proof term to Coq ... ")
     end in
   let tac_start_time = System.get_time () in
+  let term = EConstr.of_constr term in
   let result=
     if !check then
       Proofview.V82.of_tactic (Tactics.exact_check term) gls
-- 
cgit v1.2.3