diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 10 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 10 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 2 |
4 files changed, 12 insertions, 12 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 64f9403a1c..ab6c42035f 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -36,7 +36,7 @@ let pr_with_bindings prc prlc (c,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)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -46,12 +46,12 @@ let pr_fun_ind_using prc prlc _ opt_c = 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) + hv 0 (pr_bindings prc prlc 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)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) ARGUMENT EXTEND fun_ind_using @@ -96,7 +96,7 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction true c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] END (***** debug only ***) TACTIC EXTEND snewfunind @@ -107,7 +107,7 @@ TACTIC EXTEND snewfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction false c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] END diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca608ec0ba..8c22265d66 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -24,13 +24,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 (fun (_,c) -> prc c) l + Util.prlist_with_sep spc prc 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 @@ -424,7 +424,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -434,7 +434,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 = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 02d70da74c..60616845be 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1224,7 +1224,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac (inj_open eq1)) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 0beb1e1aea..476724ba6d 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -248,7 +248,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac false (Some 1) 1 - (Rawterm.ImplicitBindings [inj_open (mkVar n)]); + (Rawterm.ImplicitBindings [mkVar n]); cont]); ]))) in |