diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-23 20:58:24 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-23 20:58:24 +0000 |
| commit | 657f394cf6de00d852bf33ea8d7f17f1daededbf (patch) | |
| tree | 9beb19c91eabb41b44eb42e783dde0499f74753b /plugins/funind | |
| parent | 7e7ea4cb3dfa0b87b5666a2b13c22b2e517abb16 (diff) | |
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
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 -> |