diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 37 |
1 files changed, 17 insertions, 20 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a43463c6..d55a6c1e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: ppconstr.ml 8878 2006-05-30 16:44:25Z herbelin $ *) (*i*) open Util @@ -117,7 +117,7 @@ let pr_optc pr = function let pr_universe = Univ.pr_uni -let pr_sort = function +let pr_rawsort = function | RProp Term.Null -> str "Prop" | RProp Term.Pos -> str "Set" | RType u -> str "Type" ++ pr_opt pr_universe u @@ -153,8 +153,8 @@ let pr_lname = function | lna -> pr_located pr_name lna let pr_or_var pr = function - | Genarg.ArgArg x -> pr x - | Genarg.ArgVar (loc,s) -> pr_lident (loc,s) + | ArgArg x -> pr x + | ArgVar (loc,s) -> pr_lident (loc,s) let pr_prim_token = function | Numeral n -> Bigint.pr_bigint n @@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = let ids = names_of_local_assums bl in match ro with CStructRec -> - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" + if List.length ids > 1 && n <> None then + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" else mt() | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}" + spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" in pr_recursive_decl pr prd dangling_with_for id bl annot t c @@ -563,7 +563,7 @@ let rec pr sep inherited a = | CHole _ -> str "_", latom | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom - | CSort (_,s) -> pr_sort s, latom + | CSort (_,s) -> pr_rawsort s, latom | CCast (_,a,_,b) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), lcast @@ -619,19 +619,16 @@ let rec strip_context n iscast t = let pr_constr_expr c = pr lsimple c let pr_lconstr_expr c = pr ltop c let pr_pattern_expr c = pr lsimple c +let pr_lpattern_expr c = pr ltop c + let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders (pr ltop) -let pr_pattern_occ prc = function - ([],c) -> prc c - | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - -let pr_unfold_occ pr_ref = function - ([],qid) -> pr_ref qid - | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) +let pr_with_occurrences pr = function + ([],c) -> pr c + | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) let pr_red_flag pr r = (if r.rBeta then pr_arg str "beta" else mt ()) ++ @@ -651,7 +648,7 @@ let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | Red false -> str "red" | Hnf -> str "hnf" - | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o + | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o | Cbv f -> if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then str "compute" @@ -661,11 +658,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function hov 1 (str "lazy" ++ pr_red_flag pr_ref f) | Unfold l -> hov 1 (str "unfold" ++ spc() ++ - prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l) + prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l) | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) | Pattern l -> hov 1 (str "pattern" ++ - pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l) + pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l) | Red true -> error "Shouldn't be accessible from user" | ExtraRedExpr s -> str s |