diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 41a068ff..52f22ee6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -13,13 +13,12 @@ open Names open Libnames open Globnames open Pp -open Errors +open CErrors open Util open Table open Extraction open Modutil open Common -open Mod_subst (***************************************) (*S Part I: computing Coq environment. *) @@ -542,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_notice (str (Buffer.contents buf)); + Feedback.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -584,8 +583,8 @@ let rec locate_ref = function | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_both_mod_and_cst q mp r; - let refs,mps = locate_ref l in refs,mp::mps + warning_ambiguous_name (q,mp,r); + let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when @@ -636,7 +635,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_notice ans + Feedback.msg_notice ans | _ -> assert false |