diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 54 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
4 files changed, 8 insertions, 58 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 580c21d40e..6b046919d3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -161,28 +161,6 @@ type 'a extra_genarg_printer = | AnonHyp n -> int n | NamedHyp id -> pr_id id - let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - - let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc prc l) - | ExplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) - | NoBindings -> mt () - - let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - let pr_clear_flag clear_flag pp x = match clear_flag with | Some false -> surround (pp x) @@ -190,7 +168,7 @@ type 'a extra_genarg_printer = | None -> pp x let pr_with_bindings prc prlc (c,bl) = - prc c ++ pr_bindings prc prlc bl + prc c ++ Miscprint.pr_bindings prc prlc bl let pr_with_bindings_arg prc prlc (clear_flag,c) = pr_clear_flag clear_flag (pr_with_bindings prc prlc) c @@ -367,30 +345,6 @@ type 'a extra_genarg_printer = | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) - let pr_esubst prc l = - let pr_qhyp = function - (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,(NamedHyp id,c)) -> - str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" - in - prlist_with_sep spc pr_qhyp l - - let pr_bindings_gen for_ex prc prlc = function - | ImplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - prlist_with_sep spc prc l) - | ExplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - pr_esubst prlc l) - | NoBindings -> mt () - - let pr_bindings prc prlc = pr_bindings_gen false prc prlc - - let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl @@ -1280,9 +1234,9 @@ let () = (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 wit_bindings - (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); + (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 19bdf2d49f..4265c416b6 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds -val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 0096abfa69..d201cf9490 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -189,7 +189,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -198,7 +198,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c in (c',if !strict_check then None else Some c) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 594c4fa15f..10c0319b26 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -589,7 +589,7 @@ let interp_uconstr ist env sigma = function } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } -let interp_gen kind ist allow_patvar flags env sigma (c,ce) = +let interp_gen kind ist pattern_mode flags env sigma (c,ce) = let constrvars = extract_ltac_constr_context ist env sigma in let vars = { Pretyping.ltac_constrs = constrvars.typed; @@ -617,7 +617,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = } in let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in - intern_gen kind_for_intern ~allow_patvar ~ltacvars env c + intern_gen kind_for_intern ~pattern_mode ~ltacvars env c in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do |