diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-17 11:09:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-17 11:09:02 +0000 |
| commit | 7422420fb651d0bcbdf31d30ec93403460420daf (patch) | |
| tree | 0b4ce75e962349e42d2756b5958e0074921e093f /translate | |
| parent | 989f3ba5d92082b0ef852f4c37146617479132d0 (diff) | |
Bug affichage Hint Extern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4928 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index ae51a552b..82f01ae0c 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -195,7 +195,7 @@ let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z -let pr_hints local db h pr_c = +let pr_hints local db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pr_aux = function | CAppExpl (_,(_,qid),[]) -> pr_reference qid @@ -215,7 +215,7 @@ let pr_hints local db h pr_c = str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c | HintsExtern (name,n,c,tac) -> - str "Extern" ++ spc() ++ int n ++ spc() ++ pr_c c ++ str" =>" ++ + str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++ spc() ++ pr_raw_tactic tac | HintsDestruct(name,i,loc,c,tac) -> str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++ @@ -928,7 +928,8 @@ let rec pr_vernac = function str "Tactic Definition " else*) (* Rec by default *) str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) - | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr + | VernacHints (local,dbnames,h) -> + pr_hints local dbnames h pr_constr pr_pattern | VernacSyntacticDefinition (id,c,None) -> hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++ pr_lconstrarg c) |