diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/vconv.ml | 6 |
3 files changed, 10 insertions, 5 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7b2d927162..3c4c2796ee 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -990,6 +990,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var id -> begin let open Context.Named.Declaration in @@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - - | Proj (p, c) -> check_rec_call renv [] c and check_nested_fix_body renv decr recArgsDecrArg body = if Int.equal decr 0 then diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 23c0c1c31b..09f7bd75cd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -851,6 +851,9 @@ let export ?except senv dir = let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; + if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then + CErrors.errorlabstrm "Safe_typing.import" + (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c729a6ce29..894f5296a8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -116,14 +116,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in |