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

---
 engine/proofview.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index b0f6d463bc..9adf947441 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -72,6 +72,7 @@ let dependent_init =
   | TCons (env, sigma, typ, t) ->
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in
+    let econstr = EConstr.Unsafe.to_constr econstr in
     let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
-- 
cgit v1.2.3