From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

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

(limited to 'tactics/elim.ml')

diff --git a/tactics/elim.ml b/tactics/elim.ml
index fe36085b8..d00e504ff 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -108,12 +108,12 @@ let decompose_these c l =
 
 let decompose_and c =
   general_decompose
-    (fun sigma (_,t) -> is_record sigma t)
+    (fun sigma (_,t) -> is_record sigma (EConstr.of_constr t))
     c
 
 let decompose_or c =
   general_decompose
-    (fun sigma (_,t) -> is_disjunction sigma t)
+    (fun sigma (_,t) -> is_disjunction sigma (EConstr.of_constr t))
     c
 
 let h_decompose l c = decompose_these c l
-- 
cgit v1.2.3