diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 23 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 10 |
2 files changed, 25 insertions, 8 deletions
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index ae3da9523a..169542e3cd 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -29,20 +29,37 @@ let pr_bindings prc prlc = function Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Rawterm.NoBindings -> mt () - let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) +(* Duplication of printing functions because "'a with_bindings" is + (internally) not uniform in 'a: indeed constr_with_bindings at the + "typed" level has type "open_constr with_bindings" instead of + "constr with_bindings"; hence, its printer cannot be polymorphic in + (prc,prlc)... *) + +let pr_with_bindings_typed prc prlc (c,bl) = + prc c ++ + hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + +let pr_fun_ind_using_typed prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings_opt - PRINTED BY pr_fun_ind_using + PRINTED BY pr_fun_ind_using_typed + RAW_TYPED AS constr_with_bindings_opt + RAW_PRINTED BY pr_fun_ind_using + GLOB_TYPED AS constr_with_bindings_opt + GLOB_PRINTED BY pr_fun_ind_using | [ "using" constr_with_bindings(c) ] -> [ Some c ] | [ ] -> [ None ] END diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 9ec02d4c48..fbf72805b7 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -23,13 +23,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + Util.prlist_with_sep spc (fun (_,c) -> prc c) l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -425,7 +425,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -435,7 +435,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) |