From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Jun 2018 13:32:35 +0200 Subject: Remove the proj_eta field of the kernel. This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel. --- checker/subtyping.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker/subtyping.ml') diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5c672d04a..6f9bf8fce 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -130,8 +130,6 @@ 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 in let check_inductive_type t1 t2 = -- cgit v1.2.3