aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r--checker/subtyping.ml4
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 =