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 /checker/subtyping.ml | |
| parent | f0ae8e82ea53ce72ddac1fb8f7f40fd1beacf787 (diff) | |
| parent | e43710b391c278ac7fcb808ec28d720b4317660c (diff) | |
Merge PR #7714: Remove primitive-projection related data from the kernel
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5c672d04a..f4ae02084 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -130,9 +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 -> fst x.proj_eta); - check (eq_constr) (fun x -> snd x.proj_eta); - check (eq_constr) (fun x -> x.proj_body); true + true in let check_inductive_type t1 t2 = |