diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 15:26:20 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-17 11:44:04 +0200 |
commit | e43710b391c278ac7fcb808ec28d720b4317660c (patch) | |
tree | 00c9b48f65ed5567e1fcac31a344944d6ea148b9 /kernel/indtypes.mli | |
parent | a4839aa1ff076a8938ca182615a93d6afe748860 (diff) |
Remove the proj_body field from the kernel.
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
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) |