From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 8 Nov 2016 10:57:05 +0100
Subject: Cases API using EConstr.

---
 plugins/firstorder/formula.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 79f185d18..60e9196af 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -54,7 +54,7 @@ let construct_nhyps ind gls =
 let ind_hyps nevar ind largs gls=
   let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
   let myhyps t =
-    let t1=prod_applist t largs in
+    let t1=Term.prod_applist t largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
       fst (decompose_prod_assum t2) in
     Array.map myhyps types
-- 
cgit v1.2.3