diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index add71a8b09..67946e3a28 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -676,6 +676,11 @@ let rec extern inctx scopes vars r = let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) + + | RRecord (loc,w,l) -> + let t' = Option.map (extern inctx scopes vars) w in + let l' = List.map (fun (id, c) -> (id, extern inctx scopes vars c)) l in + CRecord (loc, t', l') | RCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = |