diff options
| author | Pierre Letouzey | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /tactics | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c802ae984c..cd265843d3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -696,7 +696,7 @@ let rec message_of_value gl v = else if has_type v (topwit wit_unit) then str "()" else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v) else if has_type v (topwit wit_intro_pattern) then - pr_intro_pattern (out_gen (topwit wit_intro_pattern) v) + Miscprint.pr_intro_pattern (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_constr_context) then pr_constr_env (pf_env gl) (out_gen (topwit wit_constr_context) v) else match Value.to_list v with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fe26bbb2db..d1b096048d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2085,7 +2085,7 @@ let check_unused_names names = if not (List.is_empty names) && Flags.is_verbose () then msg_warning (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") - ++ str": " ++ prlist_with_sep spc pr_intro_pattern names) + ++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names) let rec consume_pattern avoid id isdep gl = function | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), []) @@ -3380,7 +3380,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = let new_induct_gen_l isrec with_evars elim (eqname,names) lc = if not (Option.is_empty eqname) then errorlabstrm "" (str "Do not know what to do with " ++ - pr_intro_pattern (Option.get eqname)); + Miscprint.pr_intro_pattern (Option.get eqname)); let newlc = ref [] in let letids = ref [] in let rec atomize_list l = |