diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 08:27:51 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-19 08:27:51 +0200 |
| commit | 981864d47efca1d42f43dc5b7c5439638a86f315 (patch) | |
| tree | a835613a0143b6cfc2ab8f94361afda62840954e /kernel/indtypes.mli | |
| parent | f0ae8e82ea53ce72ddac1fb8f7f40fd1beacf787 (diff) | |
| parent | e43710b391c278ac7fcb808ec28d720b4317660c (diff) | |
Merge PR #7714: Remove primitive-projection related data from the kernel
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a38172c2..45228e35e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_projections : pinductive -> Id.t -> Id.t -> +val compute_projections : pinductive -> int -> Context.Rel.t -> int array -> int array -> Context.Rel.t -> Context.Rel.t -> (Constant.t array * projection_body array) |