diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 349d5df8..275e179e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 9304 2006-10-28 09:58:16Z herbelin $ *) +(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *) (*i*) open Util @@ -215,7 +215,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c,_,t) -> c, t + | CCast(_,c, CastConv (_,t)) -> c, t | _ -> c, CHole dummy_loc in hov 1 (surround (pr_lname na ++ pr_opt_type pr_c topt ++ @@ -566,10 +566,13 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_rawsort s, latom - | CCast (_,a,k,b) -> - let s = match k with CastConv VMcast -> "<:" | _ -> ":" in + | CCast (_,a,CastConv (k,b)) -> + let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), lcast + | CCast (_,a,CastCoerce) -> + hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), + lcast | CNotation (_,"( _ )",[t]) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env @@ -590,7 +593,7 @@ let pr = pr mt let rec strip_context n iscast t = if n = 0 then - [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t + [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t else match t with | CLambdaN (loc,(nal,t)::bll,c) -> let n' = List.length nal in @@ -613,7 +616,7 @@ let rec strip_context n iscast t = | CArrow (loc,t,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawAssum ([loc,Anonymous],t) :: bl', c - | CCast (_,c,_,_) -> strip_context n false c + | CCast (_,c,_) -> strip_context n false c | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c |