File tree Expand file tree Collapse file tree 1 file changed +2
-3
lines changed Expand file tree Collapse file tree 1 file changed +2
-3
lines changed Original file line number Diff line number Diff line change @@ -161,10 +161,9 @@ prefix-indc Prefix K (pr K NewName) :-
161161
162162dispatch (indt GR) Prefix Clauses :- !, do! [
163163 Ind = global (indt GR),
164- coq.env.indt GR _ Luno Lno Ty Knames Ktypes,
164+ coq.env.indt GR _ _ Lno Ty Knames Ktypes,
165165
166166 LnoR is 2 * Lno,
167- LunoR is 2 * Luno,
168167
169168 pi new_name\ sigma KnamesR KtypesR TyR\ (
170169 (reali Ind (global (indt new_name)) ==>
@@ -178,7 +177,7 @@ dispatch (indt GR) Prefix Clauses :- !, do! [
178177
179178 coq.ensure-fresh-global-id NewName FNewName,
180179 coq.build-indt-decl
181- (pr new_name FNewName) tt LunoR LnoR {coq.subst-fun [Ind] TyR} KnamesR KtypesR DeclR
180+ (pr new_name FNewName) tt LnoR LnoR {coq.subst-fun [Ind] TyR} KnamesR KtypesR DeclR
182181 ),
183182
184183 std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param1 generates illtyped inductive",
You can’t perform that action at this time.
0 commit comments