diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
commit | 6497f27021fec4e01f2182014f2bb1989b4707f9 (patch) | |
tree | 473be7e63895a42966970ab6a70998113bc1bd59 /translate | |
parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) |
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'translate')
-rw-r--r-- | translate/ppconstrnew.ml | 53 | ||||
-rw-r--r-- | translate/ppconstrnew.mli | 2 | ||||
-rw-r--r-- | translate/pptacticnew.mli | 4 | ||||
-rw-r--r-- | translate/ppvernacnew.ml | 4 | ||||
-rw-r--r-- | translate/ppvernacnew.mli | 2 |
5 files changed, 37 insertions, 28 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 7d2feaf2..f75f767d 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.2 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: ppconstrnew.ml,v 1.62.2.4 2004/12/29 10:17:11 herbelin Exp $ *) (*i*) open Ast @@ -367,28 +367,31 @@ let rec split_fix n typ def = let (bl,typ,def) = split_fix (n-1) typ def in (LocalRawAssum ([na],t)::bl,typ,def) -let pr_recursive_decl pr id bl annot t c = +let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = + let pr_body = + if dangling_with_for then pr_dangling else pr in pr_id id ++ str" " ++ hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ - pr_sep_com (fun () -> brk(1,2)) (pr ltop) c + pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c -let pr_fixdecl pr (id,n,bl,t,c) = +let pr_fixdecl pr prd dangling_with_for (id,n,bl,t,c) = let annot = let ids = names_of_local_assums bl in if List.length ids > 1 then spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" else mt() in - pr_recursive_decl pr id bl annot t c + pr_recursive_decl pr prd dangling_with_for id bl annot t c -let pr_cofixdecl pr (id,bl,t,c) = - pr_recursive_decl pr id bl (mt()) t c +let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) = + pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function | [] -> anomaly "(co)fixpoint with no definition" - | [d1] -> pr_decl d1 + | [d1] -> pr_decl false d1 | dl -> - prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++ + prlist_with_sep (fun () -> fnl() ++ str "with ") + (pr_decl true) dl ++ fnl() ++ str "for " ++ pr_id id let pr_arg pr x = spc () ++ pr x @@ -462,16 +465,15 @@ let rec pr sep inherited a = let (strm,prec) = match a with | CRef r -> pr_reference r, latom | CFix (_,id,fix) -> - let p = hov 0 (str"fix " ++ - pr_recursive (pr_fixdecl (pr mt)) (snd id) fix) in - if List.length fix = 1 & prec_less (fst inherited) ltop - then surround p, latom else p, lfix + hov 0 (str"fix " ++ + pr_recursive + (pr_fixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) fix), + lfix | CCoFix (_,id,cofix) -> - let p = - hov 0 (str "cofix " ++ - pr_recursive (pr_cofixdecl (pr mt)) (snd id) cofix) in - if List.length cofix = 1 & prec_less (fst inherited) ltop - then surround p, latom else p, lfix + hov 0 (str "cofix " ++ + pr_recursive + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) cofix), + lfix | CArrow (_,a,b) -> hov 0 (pr mt (larrow,L) a ++ str " ->" ++ pr (fun () ->brk(1,0)) (-larrow,E) b), @@ -530,8 +532,9 @@ let rec pr sep inherited a = v 0 (hv 0 (str "match" ++ brk (1,2) ++ hov 0 ( - prlist_with_sep sep_v (pr_case_item (pr mt)) c - ++ pr_case_type (pr mt) rtntypopt) ++ + prlist_with_sep sep_v + (pr_case_item (pr_dangling_with_for mt)) c + ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++ spc () ++ str "with") ++ prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), latom @@ -579,7 +582,7 @@ let rec pr sep inherited a = hv 0 ( str (if style=MatchStyle then "old_match " else "match ") ++ pr mt ltop c ++ - pr_return_type (pr mt) po ++ + pr_return_type (pr_dangling_with_for mt) po ++ str " with" ++ brk (1,0) ++ hov 0 (prlist (fun b -> str "| ??? =>" ++ pr spc ltop b ++ fnl ()) bl) ++ @@ -604,6 +607,11 @@ let rec pr sep inherited a = pr_with_comments loc (sep() ++ if prec_less prec inherited then strm else surround strm) +and pr_dangling_with_for sep inherited a = + match a with + | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a + | _ -> pr sep inherited a + let pr = pr mt let rec abstract_constr_expr c = function @@ -768,8 +776,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l) | Red true -> error "Shouldn't be accessible from user" - | ExtraRedExpr (s,c) -> - hov 1 (str s ++ pr_arg pr_constr c) + | ExtraRedExpr s -> str s let rec pr_may_eval test prc prlc pr2 = function | ConstrEval (r,c) -> diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index 4477728c..4a488499 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstrnew.mli,v 1.16.2.1 2004/07/16 19:31:52 herbelin Exp $ *) +(*i $Id: ppconstrnew.mli,v 1.16.2.2 2005/01/21 17:17:20 herbelin Exp $ i*) open Pp open Environ diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli index 2558413f..b49b9e56 100644 --- a/translate/pptacticnew.mli +++ b/translate/pptacticnew.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptacticnew.mli,v 1.6.2.1 2004/07/16 19:31:52 herbelin Exp $ *) +(*i $Id: pptacticnew.mli,v 1.6.2.3 2005/01/21 17:17:20 herbelin Exp $ i*) open Pp open Genarg @@ -17,6 +17,8 @@ open Names val qsnew : string -> std_ppcmds +val pr_intro_pattern : intro_pattern_expr -> std_ppcmds + val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 246253eb..bfcbee43 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.2 2004/07/16 20:48:17 herbelin Exp $ *) +(* $Id: ppvernacnew.ml,v 1.95.2.3 2004/10/12 10:10:29 herbelin Exp $ *) open Pp open Names @@ -622,7 +622,7 @@ let rec pr_vernac = function hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++ (match bl with | [] -> mt() - | _ -> error "Statements with local binders no longer supported") + | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli index 73101a1a..4506b811 100644 --- a/translate/ppvernacnew.mli +++ b/translate/ppvernacnew.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernacnew.mli,v 1.3.2.1 2004/07/16 19:31:52 herbelin Exp $ *) +(*i $Id: ppvernacnew.mli,v 1.3.2.2 2005/01/21 17:17:20 herbelin Exp $ i*) open Pp open Genarg |