diff options
| author | msozeau | 2007-03-19 16:54:25 +0000 |
|---|---|---|
| committer | msozeau | 2007-03-19 16:54:25 +0000 |
| commit | 38ff8d2b59a481ba489400ea194fdd78c6c2d5e1 (patch) | |
| tree | b0c539c86860a372b7356e6245e8db4fa50df16a /parsing/ppconstr.ml | |
| parent | 293675b06262698ba3b1ba30db8595bedd5c55ae (diff) | |
Add a parameter to QuestionMark evar kind to say it can be turned into an obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 901866523f..f0a44311bc 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -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 |