diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cae67c3e7..a5302b54d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -29,11 +29,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id ++ str + ((Id.print id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id++str" is already declared as a generalizable identifier")) + ((Id.print id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -80,7 +80,7 @@ let is_freevar ids env x = let ungeneralizable loc id = user_err ?loc ~hdr:"Generalization" - (str "Unbound and ungeneralizable variable " ++ pr_id id) + (str "Unbound and ungeneralizable variable " ++ Id.print id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -152,7 +152,7 @@ let combine_params avoid fn applied needed = | Anonymous -> false in if not (List.exists is_id needed) then - user_err ?loc (str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ?loc (str "Wrong argument name: " ++ Id.print id); true | _ -> false) applied in |