aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.ide2
-rw-r--r--ide/coq.ml6
-rw-r--r--ide/preferences.ml2
-rw-r--r--kernel/safe_typing.ml36
-rw-r--r--test-suite/bugs/closed/bug_9526.v30
5 files changed, 57 insertions, 19 deletions
diff --git a/Makefile.ide b/Makefile.ide
index 23ce83d263..db1cc3746d 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
.PHONY: ide-toploop ide-byteloop ide-optloop
# target to build CoqIde (native version) and the stuff needed to lauch it
-coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO)
+coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) $(TOPBIN)
# target to build CoqIde (in native and byte versions), and no more
# NB: this target is used in the opam package coq-coqide
diff --git a/ide/coq.ml b/ide/coq.ml
index 91cd448eda..e7eea4ced2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -119,7 +119,7 @@ let rec filter_coq_opts args =
and asks_for_coqtop args =
let pb_mes = GWindow.message_dialog
- ~message:"Failed to load coqtop. Reset the preference to default ?"
+ ~message:"Failed to load coqidetop. Reset the preference to default ?"
~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
match pb_mes#run () with
| `YES ->
@@ -130,7 +130,7 @@ and asks_for_coqtop args =
| `DELETE_EVENT | `NO ->
let () = pb_mes#destroy () in
let cmd_sel = GWindow.file_selection
- ~title:"Coqtop to execute (edit your preference then)"
+ ~title:"coqidetop to execute (edit your preference then)"
~filename:(coqtop_path ()) ~urgency_hint:true () in
match cmd_sel#run () with
| `OK ->
@@ -419,7 +419,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
let title = "Warning" in
let icon = (warn_image ())#coerce in
let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in
- let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in
+ let ans = GToolbox.question_box ~title ~buttons ~icon "coqidetop died badly." in
if ans = 2 then (!save_all (); GtkMain.Main.quit ())
else if ans = 3 then GtkMain.Main.quit ()
| Planned -> ()
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4aa8c92f73..1fdf54d4d1 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) parent =
let cmd_coqtop =
string
~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
- " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
+ " coqidetop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
let cmd_coqc = pstring " coqc" cmd_coqc in
let cmd_make = pstring " make" cmd_make in
let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index dc15d9d25e..a05f7b9b04 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1194,39 +1194,46 @@ let register_inline kn senv =
let cb = {cb with const_inline_code = true} in
let env = add_constant kn cb env in { senv with env}
-let check_register_ind (mind,i) r env =
- let mb = Environ.lookup_mind mind env in
- let check_if b s =
+let check_register_ind ind r env =
+ let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in
+ let check_if b msg =
if not b then
- CErrors.user_err ~hdr:"check_register_ind" (Pp.str s) in
- check_if (Int.equal (Array.length mb.mind_packets) 1) "A non mutual inductive is expected";
- let ob = mb.mind_packets.(i) in
+ CErrors.user_err ~hdr:"check_register_ind" msg in
+ check_if (Int.equal (Array.length mb.mind_packets) 1) Pp.(str "A non mutual inductive is expected");
+ let is_monomorphic = function Monomorphic _ -> true | Polymorphic _ -> false in
+ check_if (is_monomorphic mb.mind_universes) Pp.(str "A universe monomorphic inductive type is expected");
+ check_if (not @@ Inductive.is_private spec) Pp.(str "A non-private inductive type is expected");
+ let check_nparams n =
+ check_if (Int.equal mb.mind_nparams n) Pp.(str "An inductive type with " ++ int n ++ str " parameters is expected")
+ in
let check_nconstr n =
check_if (Int.equal (Array.length ob.mind_consnames) n)
- ("an inductive type with "^(string_of_int n)^" constructors is expected")
+ Pp.(str "an inductive type with " ++ int n ++ str " constructors is expected")
in
let check_name pos s =
check_if (Id.equal ob.mind_consnames.(pos) (Id.of_string s))
- ("the "^(string_of_int (pos + 1))^
- "th constructor does not have the expected name: " ^ s) in
+ Pp.(str"the " ++ int (pos + 1) ++ str
+ "th constructor does not have the expected name: " ++ str s) in
let check_type pos t =
check_if (Constr.equal t ob.mind_user_lc.(pos))
- ("the "^(string_of_int (pos + 1))^
+ Pp.(str"the " ++ int (pos + 1) ++ str
"th constructor does not have the expected type") in
let check_type_cte pos = check_type pos (Constr.mkRel 1) in
match r with
| CPrimitives.PIT_bool ->
+ check_nparams 0;
check_nconstr 2;
check_name 0 "true";
check_type_cte 0;
check_name 1 "false";
check_type_cte 1
| CPrimitives.PIT_carry ->
+ check_nparams 1;
check_nconstr 2;
let test_type pos =
let c = ob.mind_user_lc.(pos) in
- let s = "the "^(string_of_int (pos + 1))^
- "th constructor does not have the expected type" in
+ let s = Pp.(str"the " ++ int (pos + 1) ++ str
+ "th constructor does not have the expected type") in
check_if (Constr.isProd c) s;
let (_,d,cd) = Constr.destProd c in
check_if (Constr.is_Type d) s;
@@ -1240,11 +1247,11 @@ let check_register_ind (mind,i) r env =
check_name 1 "C1";
test_type 1;
| CPrimitives.PIT_pair ->
+ check_nparams 2;
check_nconstr 1;
check_name 0 "pair";
let c = ob.mind_user_lc.(0) in
- let s = "the "^(string_of_int 1)^
- "th constructor does not have the expected type" in
+ let s = Pp.str "the constructor does not have the expected type" in
begin match Term.decompose_prod c with
| ([_,b;_,a;_,_B;_,_A], codom) ->
check_if (is_Type _A) s;
@@ -1255,6 +1262,7 @@ let check_register_ind (mind,i) r env =
| _ -> check_if false s
end
| CPrimitives.PIT_cmp ->
+ check_nparams 0;
check_nconstr 3;
check_name 0 "Eq";
check_type_cte 0;
diff --git a/test-suite/bugs/closed/bug_9526.v b/test-suite/bugs/closed/bug_9526.v
new file mode 100644
index 0000000000..344d42083f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9526.v
@@ -0,0 +1,30 @@
+Primitive int := #int63_type.
+
+Module bad1.
+Polymorphic Inductive badcarry1 (A:Type) : Type :=
+| C0: A -> badcarry1 A
+| C1: A -> badcarry1 A.
+
+Fail Register badcarry1 as kernel.ind_carry.
+
+End bad1.
+
+Module bad2.
+
+Inductive badcarry2 (A:Set) : Set :=
+| C0: A -> badcarry2 A
+| C1: A -> badcarry2 A.
+
+Fail Register badcarry2 as kernel.ind_carry.
+
+End bad2.
+
+Module bad3.
+
+Inductive badcarry3 : Type -> Type :=
+| C0: forall A, A -> badcarry3 A
+| C1: forall A, A -> badcarry3 A.
+
+Fail Register badcarry3 as kernel.ind_carry.
+
+End bad3.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:38:34 +0000