Skip to content

Commit

Permalink
Adapt to Coq PR #19404
Browse files Browse the repository at this point in the history
  • Loading branch information
herbelin committed Jul 20, 2024
1 parent 7830cea commit e1a9e73
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/coq_elpi_builtins.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3194,7 +3194,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,([],[])),Id.Set.empty,Notation_term.NtnTypeConstr)) :: vars in
(id, Notation_term.(NtnTypeVar (((Notation_ops.constr_some_level,([],[])),Id.Set.empty),NtnTypeVarConstr NtnConstrForConstrAndPatternForPattern))) :: vars in
let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum(name,ty)) env in
aux vars nenv env (n-1) t
| _ ->
Expand All @@ -3205,7 +3205,7 @@ Supported attributes:
let nenv =
{
Notation_term.ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
ninterp_raw_types = [];
} in
aux vars nenv env nargs term
in
Expand Down

0 comments on commit e1a9e73

Please sign in to comment.