From 380690d4fadcff2148d4633ad7bb214d2e78af01 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 28 Nov 2022 21:03:34 -0500 Subject: [PATCH] Use `context` in `PCUICAst.mutual_inductive_entry` --- pcuic/theories/PCUICAst.v | 2 +- pcuic/theories/utils/PCUICAstUtils.v | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v index 0a79cb462..f2e4f3c72 100644 --- a/pcuic/theories/PCUICAst.v +++ b/pcuic/theories/PCUICAst.v @@ -1309,7 +1309,7 @@ Record mutual_inductive_entry := { If so, is it primitive, using binder name [ident] for the record in primitive projections ? *) mind_entry_finite : recursivity_kind; - mind_entry_params : list (ident * local_entry); + mind_entry_params : context; mind_entry_inds : list one_inductive_entry; mind_entry_universes : universes_decl; mind_entry_private : option bool diff --git a/pcuic/theories/utils/PCUICAstUtils.v b/pcuic/theories/utils/PCUICAstUtils.v index d67b0be8d..8036b90fe 100644 --- a/pcuic/theories/utils/PCUICAstUtils.v +++ b/pcuic/theories/utils/PCUICAstUtils.v @@ -233,9 +233,7 @@ Proof. destruct typ as [[names types] _]. apply (List.firstn decl.(ind_npars)) in names. apply (List.firstn decl.(ind_npars)) in types. - refine (List.combine _ _). - exact (List.map string_of_aname names). - exact (List.map LocalAssum types). + refine (map (fun '(x, ty) => vass x ty) (combine names types)). - refine (List.map _ decl.(ind_bodies)). intros []. refine {| mind_entry_typename := ind_name0;