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

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

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0a7938069f..83fc48623c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1150,7 +1150,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let info_array =
 	      Array.mapi
 		(fun i types ->
-		   let types = prod_applist types (List.rev_map var_of_decl princ_params) in
+		   let types = Term.prod_applist types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
 		     name = Nameops.out_name (fresh_id names.(i));
 		     types = types;
-- 
cgit v1.2.3