diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e498d979de..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 = @@ -119,13 +119,14 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li in aux bound l binders let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = - let rec vars bound vs t = match t with - | { loc; CAst.v = GVar id } -> + let rec vars bound vs c = match DAst.get c with + | GVar id -> + let loc = c.CAst.loc in if is_freevar bound (Global.env ()) id then if Id.List.mem_assoc_sym id vs then vs else (Loc.tag ?loc id) :: vs else vs - | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c + | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vars = List.rev (vars bound [] rt) in List.iter (fun (loc, id) -> @@ -151,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 @@ -253,11 +254,11 @@ let implicits_of_glob_constr ?(with_products=true) l = (ExplByPos (i, name), (true, true, true)) :: l | _ -> l in - let rec aux i { loc; CAst.v = c } = + let rec aux i c = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match c with + match DAst.get c with | GProd (na, bk, t, b) -> if with_products then abs na bk b else |