We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 84c4b5d commit 3b75595Copy full SHA for 3b75595
hb.elpi
@@ -2095,7 +2095,8 @@ copy-indt-decl (parameter ID I Ty D) (parameter ID I Ty1 D1) :-
2095
@pi-parameter ID Ty1 x\ copy-indt-decl (D x) (D1 x).
2096
copy-indt-decl (inductive ID CO A D) (inductive ID CO A1 D1) :-
2097
copy-arity A A1,
2098
- @pi-inductive ID A1 i\ std.map (D i) copy-constructor (D1 i).
+ coq.id->name ID N, coq.arity->term A1 T, @pi-decl N T i\ std.map (D i) copy-constructor (D1 i).
2099
+ % @pi-inductive ID A1 i\ std.map (D i) copy-constructor (D1 i). % requires Coq-Elpi 1.9.x
2100
copy-indt-decl (record ID T IDK F) (record ID T1 IDK F1) :-
2101
copy T T1,
2102
copy-fields F F1.
0 commit comments