From b5a0e384b405f64fd0854d5e88b55e8c2a159c02 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 11:02:09 -0400
Subject: Univs: fix bug #4375, accept universe binders on (co)-fixpoints

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

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 47c67ed2aa..3dbd438061 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -592,7 +592,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in
+  let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
     with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
   let fixpoint_exprl_with_new_bl = 
-- 
cgit v1.2.3