diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:14:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:14:19 +0000 |
| commit | 98e20d5bc1250bf83940b7b9ea7b049e7834abfb (patch) | |
| tree | 950e570bfb1aa179165d4e785d426bbb9688b436 /translate/ppvernacnew.ml | |
| parent | 95d4aef96fb7b490b188afe66e8345428e9706ee (diff) | |
Mise en place possibilité de définitions locales dans les paramètres des records
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index f3a0798ef..a8ccc7dcf 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -324,14 +324,6 @@ let pr_vbinders l = let pr_binders_arg bl = if bl = [] then mt () else spc () ++ pr_binders bl -let pr_sbinders sbl = - if sbl = [] then mt () else - let bl = - List.map (fun (id,c) -> - let c = anonymize_binder (Name id) c in - LocalRawAssum ([(dummy_loc,Name id)],c)) sbl in - pr_binders bl ++ spc () - let pr_onescheme (id,dep,ind,s) = hov 0 (pr_id id ++ str" :=") ++ spc() ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") @@ -843,8 +835,8 @@ pr_vbinders bl ++ spc()) pr_lconstr b)) in hov 2 (str (if b then "Record" else "Structure") ++ - (if oc then str" > " else str" ") ++ pr_id name ++ spc() ++ - pr_sbinders ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++ + (if oc then str" > " else str" ") ++ pr_id name ++ + pr_binders_arg ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++ (match c with | None -> mt() | Some sc -> pr_id sc) ++ |