diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cae67c3e70..519f2480ba 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 = @@ -94,8 +94,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c - | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names 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 |