From 657f394cf6de00d852bf33ea8d7f17f1daededbf Mon Sep 17 00:00:00 2001 From: jforest Date: Fri, 23 Jul 2010 20:58:24 +0000 Subject: correcting a bug in funind introduced in r 13292 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13320 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/indfun.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ba9bde01c..346330b9a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -598,11 +598,13 @@ let id_of_name = function bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ')) | _ -> assert false +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),_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - List.map (Constrextern.extern_constr false (Global.env ())) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> -- cgit v1.2.3