diff options
| author | herbelin | 2003-06-14 09:15:38 +0000 |
|---|---|---|
| committer | herbelin | 2003-06-14 09:15:38 +0000 |
| commit | 3f1769a8002addec9f53969affd6b4cee1ccbbea (patch) | |
| tree | cab9b33832658113f646ebc38d78cd0bb2c83de3 /translate | |
| parent | 8ddd9ba6efcd32a13b4517a4e80c5fc035a951a8 (diff) | |
Ajout option Local à Hint, Hints et HintDestruct
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index f6577dc143..7f84974574 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -155,7 +155,7 @@ let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z -let pr_hints db h pr_c = +let pr_hints local db h pr_c = let db_name = function | [] -> (false , mt()) | c1::c2 -> match c1 with @@ -169,38 +169,42 @@ let pr_hints db h pr_c = | HintsResolve l -> let (f,dbn) = db_name l in if f then - hov 1 (str"Hint " ++ dbn ++ spc() ++ opth ++ + hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++ str" :=" ++ spc() ++ str"Resolve" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 - (str"Hints Resolve " ++ + (str"Hints " ++ pr_locality local ++ str "Resolve " ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) | HintsImmediate l -> let (f,dbn) = db_name l in if f then - hov 1 (str"Hint " ++ dbn ++ spc() ++ opth ++ + hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++ str" :=" ++ spc() ++ str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) else hov 1 - (str"Hints Immediate " ++ + (str"Hints " ++ pr_locality local ++ str "Immediate " ++ prlist_with_sep sep pr_aux (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) | HintsUnfold l -> let (f,dbn) = db_name l in if f then - hov 1 (str"Hint" ++ spc() ++ dbn ++ spc() ++ opth ++ + hov 1 (str"Hint" ++ spc() ++ pr_locality local ++ + dbn ++ spc() ++ opth ++ str" :=" ++ spc() ++ str"Unfold" ++ spc() ++ prlist_with_sep sep pr_reference (List.map snd l)) else hov 1 - (str"Hints Unfold " ++ prlist_with_sep sep pr_reference + (str"Hints " ++ pr_locality local ++ str "Unfold " ++ + prlist_with_sep sep pr_reference (List.map snd l) ++ spc() ++ opth) | HintsConstructors (n,c) -> - hov 1 (str"Hint " ++ pr_id n ++ spc() ++ opth ++ str" :=" ++ + hov 1 (str"Hint " ++ pr_locality local ++ + pr_id n ++ spc() ++ opth ++ str" :=" ++ spc() ++ str"Constructors" ++ spc() ++ pr_reference c) | HintsExtern (name,n,c,tac) -> - hov 1 (str"Hint " ++ pr_id name ++ spc() ++ opth ++ str" :=" ++ + hov 1 (str"Hint " ++ pr_locality local ++ + pr_id name ++ spc() ++ opth ++ str" :=" ++ spc() ++ str"Extern " ++ int n ++ spc() ++ pr_c c ++ spc() ++ pr_raw_tactic tac) @@ -818,9 +822,10 @@ 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 (dbnames,h) -> pr_hints dbnames h pr_constr - | VernacHintDestruct (id,loc,c,i,tac) -> - hov 2 (str"HintDestruct " ++ pr_destruct_location loc ++ spc() ++ + | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr + | VernacHintDestruct (local,id,loc,c,i,tac) -> + hov 2 (str"HintDestruct " ++ pr_locality local ++ + pr_destruct_location loc ++ spc() ++ pr_id id ++ pr_constrarg c ++ pr_intarg i ++ spc() ++ str"[" ++ pr_raw_tactic tac ++ str"]") | VernacSyntacticDefinition (id,c,None) -> |