diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.mli | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 3 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 |
7 files changed, 4 insertions, 12 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 11958c9108..d74c96af84 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -860,7 +860,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && - eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8c364602e9..2f11f3dd6b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -193,8 +193,6 @@ type 'a extended_conversion_function = 'a -> 'a -> unit exception NotConvertible -exception NotConvertibleVect of int - (* Convertibility of sorts *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0408dbf057..7dcafb7d7b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -27,7 +27,6 @@ val nf_betaiota : env -> constr -> constr s conversion functions *) exception NotConvertible -exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index edb1d0a02e..673f025c75 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -842,7 +842,7 @@ let check_mind mie lab = let add_mind l mie senv = let () = check_mind mie l in let kn = MutInd.make2 senv.modpath l in - let mib = Term_typing.translate_mind senv.env kn mie in + let mib = Indtypes.check_inductive senv.env kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f773f800c6..faa4411e92 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -371,7 +371,3 @@ let translate_local_def env _id centry = | Undef _ | Primitive _ -> assert false in c, decl.cook_relevance, typ - -(* Insertion of inductive types. *) - -let translate_mind env kn mie = Indtypes.check_inductive env kn mie diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index d34c28138e..1fa5eca2e3 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -35,9 +35,6 @@ val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -val translate_mind : - env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body - val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be878dd99b..12ffbf4357 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -26,6 +26,8 @@ open Type_errors module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +exception NotConvertibleVect of int + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = |