From 2462f828d342c91f1a435bacf94e17126eb53252 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Oct 2003 11:18:05 +0000 Subject: Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de SearchNamed dans SearchAbout git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4697 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/ppvernacnew.ml | 40 ++++++++++------------------------------ 1 file changed, 10 insertions(+), 30 deletions(-) (limited to 'translate/ppvernacnew.ml') diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 363593d78..b8bcf8cbd 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -51,31 +51,7 @@ let pr_import_module = (* We assume List is never imported with "Import" ... *) Libnames.pr_reference -let pr_reference r = - let loc = loc_of_reference r in - try match Nametab.extended_locate (snd (qualid_of_reference r)) with - | TrueGlobal ref -> - pr_with_comments loc - (pr_reference (Constrextern.extern_reference loc Idset.empty ref)) - | SyntacticDef kn -> - let is_coq_root d = - let d = repr_dirpath d in - d <> [] & string_of_id (list_last d) = "Coq" in - let dir,id = repr_path (sp_of_syntactic_definition kn) in - let r = - if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then - (match string_of_id id with - | "refl_eqT" -> - Constrextern.extern_reference dummy_loc Idset.empty - (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.refl) - | "sym_eqT" -> - Constrextern.extern_reference dummy_loc Idset.empty - (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.sym) - | _ -> r) - else r - in pr_with_comments loc (pr_reference r) - with Not_found -> - error_global_not_found (snd (qualid_of_reference r)) +let pr_reference = Ppconstrnew.pr_reference let sep_end () = str"." @@ -169,11 +145,15 @@ let pr_in_out_modules = function | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l +let pr_search_about = function + | Search.SearchRef r -> pr_reference r + | Search.SearchString s -> qsnew s + let pr_search a b pr_p = match a with | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout qid -> str"SearchAbout" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b + | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b | SearchNamed sl -> str"SearchNamed" ++ spc() ++ prlist_with_sep spc qsnew sl ++ pr_in_out_modules b let pr_locality local = if local then str "Local " else str "" @@ -305,7 +285,7 @@ let without_translation f x = with e -> Options.make_translate old; Options.v7:=oldv7; raise e let pr_decl_notation prc = - pr_opt (fun (ntn,c,scopt) -> + pr_opt (fun (ntn,c,scopt) -> fnl () ++ str "where " ++ qsnew ntn ++ str " := " ++ without_translation prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt) @@ -731,7 +711,7 @@ let rec pr_vernac = function str key ++ spc() ++ pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ spc() ++ pr_type s ++ - str" :=") ++ pr_constructor_list lc ++ fnl () ++ fnl () ++ + str" :=") ++ pr_constructor_list lc ++ fnl () ++ pr_decl_notation pr_constr ntn in (* Copie simplifiée de command.ml pour déclarer les notations locales *) @@ -800,11 +780,11 @@ let rec pr_vernac = function true (abstract_rawconstr (CCast (dummy_loc,def,type_)) bl) in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_type c) type_ - ++ str" :=" ++ brk(1,1) ++ ppc ++ fnl () ++ fnl () ++ + ++ str" :=" ++ brk(1,1) ++ ppc ++ pr_decl_notation pr_constr ntn in hov 1 (str"Fixpoint" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs) + prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) | VernacCoFixpoint corecs -> let pr_onecorec (id,c,def) = -- cgit v1.2.3