diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ff435bfc..4a2e5ee3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 9535 2007-01-26 09:26:08Z jforest $ *) +(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -355,12 +355,15 @@ let detype_sort = function (**********************************************************************) (* Main detyping function *) -let rec detype isgoal avoid env t = +let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable") +let set_detype_anonymous f = detype_anonymous := f + +let rec detype (isgoal:bool) avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with | Name id -> RVar (dl, id) - | Anonymous -> anomaly "detype: index to an anonymous variable" + | Anonymous -> !detype_anonymous dl n with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in RVar (dl, id_of_string s)) @@ -374,8 +377,7 @@ let rec detype isgoal avoid env t = RVar (dl, id)) | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, CastConv k, - detype isgoal avoid env c2) + RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c @@ -627,14 +629,18 @@ let rec subst_rawconstr subst raw = let ref',_ = subst_global subst ref in if ref' == ref then raw else RHole (loc,InternalHole) - | RHole (loc, (BinderType _ | QuestionMark | CasesType | + | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | TomatchTypeParameter _)) -> raw - | RCast (loc,r1,k,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1',k,r2') - + | RCast (loc,r1,k) -> + (match k with + CastConv (k,r2) -> + let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + RCast (loc,r1', CastConv (k,r2')) + | CastCoerce -> + let r1' = subst_rawconstr subst r1 in + if r1' == r1 then raw else RCast (loc,r1',k)) | RDynamic _ -> raw (* Utilities to transform kernel cases to simple pattern-matching problem *) |