diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b087431e85..3667757a2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r = insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = + (* This is to ensure that notations for coercions are used only when + the coercion is fully applied; not explicitly done yet, but we + could also expect that the notation is exactly talking about the + coercion *) match nargs with | None -> l | Some nargs -> - List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l + List.filter (fun (keyrule,pat,n as _rule) -> + match n with + | AppBoundedNotation n -> n > nargs + | AppUnboundedNotation | NotAppNotation -> false) l (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -1095,6 +1102,9 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) + | GArray(u,t,def,ty) -> + CArray(u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + in insert_entry_coercion coercion (CAst.make ?loc c) and extern_typ ?impargs (subentry,(_,scopes)) = @@ -1244,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n -> + | AppBoundedNotation n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in let args2impls = @@ -1254,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [] else try List.skipn n argsimpls with Failure _ -> [] in DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls - | None -> + | AppUnboundedNotation -> t, [], [], [] + | NotAppNotation -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | _ -> raise No_match in + | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in @@ -1469,6 +1480,9 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i | PFloat f -> GFloat f + | PArray(t,def,ty) -> + let glob_of = glob_of_pat avoid env sigma in + GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) |