From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:07:35 +0100
Subject: Inv API using EConstr.

---
 ltac/rewrite.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 0d279ae93d..f2ffb0413b 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -39,6 +39,10 @@ open Context.Named.Declaration
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  RelDecl.LocalAssum (na, inj t)
+
 (** Typeclass-based generalized rewriting. *)
 
 (** Constants used by the tactic. *)
@@ -531,7 +535,8 @@ let decompose_applied_relation env sigma (c,l) =
     | Some c -> c
     | None ->
 	let ctx,t' = Reductionops.splay_prod env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
+	let t' = EConstr.Unsafe.to_constr t' in
+	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> local_assum (n, t)) ctx)) with
 	| Some c -> c
 	| None -> error "Cannot find an homogeneous relation to rewrite."
 
-- 
cgit v1.2.3