diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 444ac5ab6d..8e49800982 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -625,8 +625,13 @@ let explicitize inctx impl (cf,f) args = CApp ((ip,f),args1@args2) | None -> let args = exprec 1 (args,impl) in - if List.is_empty args then f.CAst.v else CApp ((None, f), args) - in + if List.is_empty args then f.CAst.v else + match f.CAst.v with + | CApp (g,args') -> + (* may happen with notations for a prefix of an n-ary + application *) + CApp (g,args'@args) + | _ -> CApp ((None, f), args) in try expl () with Expl -> let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in @@ -962,6 +967,8 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, map_cast_type (extern_typ scopes vars) c') + | GInt i -> + CPrim(Numeral (Uint63.to_string i,true)) in insert_coercion coercion (CAst.make ?loc c) @@ -1307,6 +1314,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) | PSort s -> GSort s + | PInt i -> GInt i let extern_constr_pattern env sigma pat = extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) |