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

mattam82 · Nov 10, 2023 · 0d539a1 · 0d539a1
1 parent dbc5fbb
commit 0d539a1
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/src/covering.ml b/src/covering.ml
@@ -331,7 +331,7 @@ let add_wfrec_implicits rec_type c =
                                             qm_name = Anonymous;
                                             qm_record_field = None }
                     in
-                    let newarg = GHole (Evar_kinds.QuestionMark kind, Namegen.IntroAnonymous) in
+                    let newarg = GHole (GQuestionMark kind) in
                     let newarg = DAst.make ?loc newarg in
                     let before, after = List.chop nargs (mapargs args) in
                     let args' = List.append before (newarg :: after) in
@@ -745,7 +745,7 @@ let interp_arity env evd ~poly ~is_rec ~with_evars notations (((loc,i),udecl,rec
   let (arity, impls') =
     let ty = match t with
       | Some ty -> ty
-      | None -> CAst.make ?loc (Constrexpr.CHole (None, Namegen.IntroAnonymous))
+      | None -> CAst.make ?loc (Constrexpr.CHole None)
     in
     Equations_common.evd_comb1 (interp_type_evars_impls env' ?impls:None) evd ty
   in

diff --git a/src/depelim.ml b/src/depelim.ml
@@ -412,7 +412,7 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic =
      * the [rel_context]. *)
     let ty = Vars.subst_vars sigma subst concl in
     let rhs =
-      let prog = Constrexpr.CHole (None, Namegen.IntroAnonymous) in
+      let prog = Constrexpr.CHole None in
         Syntax.Program (Syntax.ConstrExpr (CAst.make prog), ([], []))
     in
     begin match patterns with

diff --git a/src/syntax.ml b/src/syntax.ml
@@ -336,7 +336,7 @@ let _chole c loc =
   let kn = Lib.make_kn c in
   let cst = Names.Constant.make kn kn in
   CAst.make ~loc
-  (CHole (Some (ImplicitArg (GlobRef.ConstRef cst, (0,None), false)), Namegen.IntroAnonymous)), None
+  (CHole (Some (GImplicitArg (GlobRef.ConstRef cst, (0,None), false)))), None
 
 let _check_linearity env sigma opats =
   let rec aux ids pats = 
@@ -355,7 +355,7 @@ let _check_linearity env sigma opats =
   in ignore (aux Id.Set.empty opats)
 
 let is_implicit_arg = function
-  | ImplicitArg _ -> true
+  | GImplicitArg _ -> true
   | _ -> false
 
 let pattern_of_glob_constr env sigma avoid patname gc =
@@ -380,7 +380,7 @@ let pattern_of_glob_constr env sigma avoid patname gc =
     PUCstr (c, nparams, List.map (DAst.map_with_loc (aux Anonymous)) l)
   and aux patname ?loc = function
     | GVar id -> PUVar (id, User)
-    | GHole (k,_) ->
+    | GHole k ->
       (match patname with
       | Name id when is_implicit_arg k -> PUVar (id, Implicit)
       | _ ->