diff options
| author | Matthieu Sozeau | 2015-10-28 11:02:09 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-28 11:02:52 -0400 |
| commit | b5a0e384b405f64fd0854d5e88b55e8c2a159c02 (patch) | |
| tree | 6f5ae6fc34acb395543c91dfd3e172d30998be7c /plugins | |
| parent | e3ec13976d39909ac6f1a82bf1b243ba8a895190 (diff) | |
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |