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 /checker | |
| 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 'checker')
| -rw-r--r-- | checker/cic.mli | 1 | ||||
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
3 files changed, 3 insertions, 4 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 94958447e..3304b032e 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -211,7 +211,6 @@ type projection_body = { proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) - proj_body : constr; (* For compatibility, the match version *) } type constant_def = diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 6f9bf8fce..f4ae02084 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -130,7 +130,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); - check (eq_constr) (fun x -> x.proj_body); true + true in let check_inductive_type t1 t2 = diff --git a/checker/values.ml b/checker/values.ml index 12fbf1ff0..45f04f88d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli +MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli *) @@ -225,7 +225,7 @@ let v_cst_def = let v_projbody = v_tuple "projection_body" - [|v_cst;Int;Int;v_constr;v_constr|] + [|v_cst;Int;Int;v_constr|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] |