From 2d4c43aad366c4946232ab46ccf7d265711bd624 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Aug 2023 13:27:24 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/17827 --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 99a0b0ef9..4cc812479 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2923,7 +2923,7 @@ Supported attributes: { nenv with Notation_term.ninterp_var_type = Id.Map.add id (Notation_term.NtnInternTypeAny None) nenv.Notation_term.ninterp_var_type }, - (id, ((Notation_ops.constr_some_level,([],[])),Notation_term.NtnTypeConstr)) :: vars in + (id, ((Notation_ops.constr_some_level,([],[])),Id.Set.empty,Notation_term.NtnTypeConstr)) :: vars in let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum(name,ty)) env in aux vars nenv env (n-1) t | _ ->