diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eb4c73791..6854a4a7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -603,12 +603,6 @@ let rec subst_rawconstr subst raw = if r1' == r1 && r2' == r2 then raw else RLetIn (loc,n,r1',r2') - | RRecord (loc,w,rl) -> - let w' = Option.smartmap (subst_rawconstr subst) w - and rl' = list_smartmap (fun (id, x) -> (id, subst_rawconstr subst x)) rl in - if w == w' && rl == rl' then raw else - RRecord (loc,w',rl') - | RCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_rawconstr subst) rtno and rl' = list_smartmap (fun (a,x as y) -> |