From 98e20d5bc1250bf83940b7b9ea7b049e7834abfb Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 6 Sep 2003 19:14:19 +0000 Subject: Mise en place possibilité de définitions locales dans les paramètres des records MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/ppvernacnew.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'translate') 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) ++ -- cgit v1.2.3