From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 tactics/autorewrite.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics/autorewrite.ml')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d656206d65..0293842975 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -285,6 +285,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     | Some c -> Some c
     | None ->
 	let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
+	let t' = EConstr.Unsafe.to_constr t' in
 	match find_rel (it_mkProd_or_LetIn t' ctx) with
 	| Some c -> Some c
 	| None -> None
-- 
cgit v1.2.3