From 9ad9c440ceae4aa52483a1ed6c77ef05f8438c36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 10 Nov 2023 16:42:12 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#18294. --- elpi-builtin.elpi | 2 +- src/coq_elpi_arg_HOAS.ml | 2 +- src/coq_elpi_builtins.ml | 8 ++++---- src/coq_elpi_utils.ml | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi index 2b0186ec6..c3dc18f8f 100644 --- a/elpi-builtin.elpi +++ b/elpi-builtin.elpi @@ -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. external pred print_constraints. % prints all constraints diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 100c7d752..9771aab3b 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -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 diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 20d25f533..d5818233b 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -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) @@ -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 @@ -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 @@ -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 diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 3a63fc9a4..8da1a03a9 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -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