From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

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

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 3ba5da149a..1e49d8cad9 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -179,6 +179,7 @@ module Btauto = struct
 
   let print_counterexample p env gl =
     let var = lapp witness [|p|] in
+    let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
-- 
cgit v1.2.3