diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 4 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 8 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 11 |
3 files changed, 14 insertions, 9 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index f75f767d..381ac2c3 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstrnew.ml,v 1.62.2.4 2004/12/29 10:17:11 herbelin Exp $ *) +(* $Id: ppconstrnew.ml,v 1.62.2.6 2005/03/08 10:13:45 herbelin Exp $ *) (*i*) open Ast @@ -118,7 +118,7 @@ let pr_optc pr = function | None -> mt () | Some x -> pr_sep_com spc pr x -let pr_universe u = str "<univ>" +let pr_universe = Univ.pr_uni let pr_sort = function | RProp Term.Null -> str "Prop" diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 80298c3e..7da30c4e 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptacticnew.ml,v 1.57.2.2 2004/07/16 19:31:52 herbelin Exp $ *) +(* $Id: pptacticnew.ml,v 1.57.2.3 2005/05/15 12:47:03 herbelin Exp $ *) open Pp open Names @@ -587,7 +587,8 @@ and pr_atom1 env = function | TacTrivial (Some []) as x -> pr_atom0 env x | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db) | TacAuto (None,Some []) as x -> pr_atom0 env x - | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAuto (n,db) -> + hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) (* | TacAutoTDB None as x -> pr_atom0 env x | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n) | TacDestructHyp (true,id) -> @@ -599,7 +600,8 @@ and pr_atom1 env = function hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)*) | TacDAuto (n,p) -> - hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p) + hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ + pr_opt int p) (* Context management *) | TacClear l -> diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index bfcbee43..2e921c4e 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernacnew.ml,v 1.95.2.3 2004/10/12 10:10:29 herbelin Exp $ *) +(* $Id: ppvernacnew.ml,v 1.95.2.4 2005/12/23 22:16:56 herbelin Exp $ *) open Pp open Names @@ -48,9 +48,12 @@ let pr_module r = Ident (loc,id_of_string s) | Qualid (loc,qid) -> Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in - let (_,dir,_) = + let dir = try - Library.locate_qualified_library (snd (qualid_of_reference r)) + Nametab.full_name_module (snd (qualid_of_reference r)) + with _ -> + try + pi2 (Library.locate_qualified_library (snd (qualid_of_reference r))) with _ -> errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r) in @@ -1032,7 +1035,7 @@ let rec pr_vernac = function | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern - | VernacLocate loc -> + | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_reference qid | LocateFile f -> str"File" ++ spc() ++ qsnew f |