Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt w.r.t. coq/coq#18294. #542

Merged
merged 1 commit into from
Nov 13, 2023
Merged

Adapt w.r.t. coq/coq#18294. #542

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion elpi-builtin.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ not _.

% [declare_constraint C Key1 Key2...] declares C blocked
% on Key1 Key2 ... (variables, or lists thereof).
external type declare_constraint any -> any -> variadic any prop.
external type declare_constraint variadic any prop.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure what's up with this, on my machine it produces the any -> any ->


external pred print_constraints. % prints all constraints

Expand Down
2 changes: 1 addition & 1 deletion src/coq_elpi_arg_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
{ finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it

let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous)
let expr_hole = CAst.make @@ Constrexpr.CHole(None)

let raw_context_decl_to_glob glob_sign fields =
let _intern_env, fields = intern_global_context ~intern_env:Constrintern.empty_internalization_env glob_sign fields in
Expand Down
8 changes: 4 additions & 4 deletions src/coq_elpi_builtins.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ let pr_econstr_env options env sigma t =
let expr = Constrextern.extern_constr env sigma t in
let expr =
let rec aux () ({ CAst.v } as orig) = match v with
| Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous)
| Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None)
| _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in
if options.hoas_holes = Some Heuristic then aux () expr else expr in
Ppconstr.pr_constr_expr_n env sigma options.pplevel expr)
Expand Down Expand Up @@ -915,7 +915,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor
| Coq_elpi_arg_HOAS.Tac.Term (t,_) ->
let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in
let rec aux () ({ CAst.v } as orig) = match v with
| Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous)
| Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None)
| _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in
Coq_elpi_arg_HOAS.Tac.Term (aux () expr)
| _ -> assert false) in
Expand Down Expand Up @@ -3120,7 +3120,7 @@ Supported attributes:
let binders, vars = List.split (CList.init nargs (fun i ->
let name = Coq_elpi_glob_quotation.mk_restricted_name i in
let lname = CAst.make @@ Name.Name (Id.of_string name) in
CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)),
CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None)),
(CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in
let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in
let sigma = get_sigma state in
Expand Down Expand Up @@ -3150,7 +3150,7 @@ Supported attributes:
let binders, vars = List.split (CList.init nargs (fun i ->
let name = Coq_elpi_glob_quotation.mk_restricted_name i in
let lname = CAst.make @@ Name.Name (Id.of_string name) in
CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)),
CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None)),
(CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in
let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in
let sigma = get_sigma state in
Expand Down
2 changes: 1 addition & 1 deletion src/coq_elpi_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ let safe_destApp sigma t =

let mkGHole =
DAst.make
(Glob_term.GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous))
(Glob_term.(GHole GInternalHole))

let mkApp ~depth t l =
match l with
Expand Down