Merge pull request #542 from ppedrot/glob-evar-kinds

LPCIC · Nov 13, 2023 · 4b050c6 · 4b050c6
2 parents f0b4b9c + 9ad9c44
commit 4b050c6
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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