From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 tactics/leminv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/leminv.ml')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 85910355e..16a048af8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -258,8 +258,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let clause = mk_clenv_type_of gls c in
-    let clause = clenv_constrain_last_binding (mkVar id) clause in
+    let clause = mk_clenv_type_of gls (EConstr.of_constr c) in
+    let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
-- 
cgit v1.2.3