diff options
| -rw-r--r-- | .gitlab-ci.yml | 14 | ||||
| -rw-r--r-- | Makefile.dune | 7 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 49 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 45 | ||||
| -rw-r--r-- | doc/stdlib/dune | 36 | ||||
| -rw-r--r-- | ide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coqide.ml | 4 | ||||
| -rw-r--r-- | ide/ideutils.ml | 19 | ||||
| -rw-r--r-- | ide/ideutils.mli | 1 | ||||
| -rw-r--r-- | ide/preferences.ml | 57 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 36 | ||||
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9526.v | 30 |
17 files changed, 215 insertions, 106 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 668f0f50f4..a1da9be20b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -346,6 +346,16 @@ doc:refman:dune: paths: - _build/default/doc/sphinx_build/html +doc:stdlib:dune: + <<: *dune-ci-template + variables: + <<: *dune-ci-template-vars + DUNE_TARGET: stdlib-html + artifacts: + <<: *dune-ci-template-artifacts + paths: + - _build/default/doc/stdlib/html + doc:refman:deploy: stage: deploy environment: @@ -357,7 +367,7 @@ doc:refman:deploy: dependencies: - doc:ml-api:odoc - doc:refman:dune - - doc:refman + - doc:stdlib:dune before_script: - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) - eval $(ssh-agent -s) @@ -375,7 +385,7 @@ doc:refman:deploy: - mkdir -p _deploy/$CI_COMMIT_REF_NAME - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman - - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib + - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - git add api refman stdlib - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" diff --git a/Makefile.dune b/Makefile.dune index 29f6fed974..da4c59af75 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,8 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt # Partial / quick developer targets -.PHONY: test-suite refman-html apidoc release # Accesory targets +.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: test-suite release # Accesory targets .PHONY: ocheck trunk ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build @@ -29,6 +30,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @echo "" @@ -81,6 +83,9 @@ test-suite: voboot refman-html: voboot dune build @refman-html +stdlib-html: voboot + dune build @stdlib-html + apidoc: voboot dune build $(DUNEOPT) @doc 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/dev/doc/MERGING.md b/dev/doc/MERGING.md index 5705857d76..3f1b470878 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -37,6 +37,9 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. +To know what files you are a code owner of in a large PR, you can run +`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. + When a PR received lots of comments or if the PR has not been opened for long and the assignee thinks that some other developers might want to comment, it is recommended that they announce their intention to merge and wait a full diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 25f983ac1e..f1733a5ebf 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2260,3 +2260,52 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 237b534d67..b81830f06b 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2094,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a98a46ba21..3e8dd25ee0 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1213,10 +1213,19 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _internal-registration-commands: + +Internal registration commands +-------------------------------- + +Due to their internal nature, the commands that are presented in this section +are not for general use. They are meant to appear only in standard libraries and +in support libraries of plug-ins. + .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries ----------------------------------------------------------------- +```````````````````````````````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 @@ -1225,5 +1234,35 @@ Exposing constants to OCaml libraries calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known where is the constant defined (file, module, library, etc.). - Due to its internal nature, this command is not for general use. It is meant - to appear only in standard libraries and in support libraries of plug-ins. + As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, + the constant is exposed to the kernel. For instance, the `Int63` module + features the following declaration: + + .. coqdoc:: + + Register bool as kernel.ind_bool. + + This makes the kernel aware of what is the type of boolean values. This + information is used for instance to define the return type of the + :g:`#int63_eq` primitive. + + .. seealso:: :ref:`primitive-integers` + +Inlining hints for the fast reduction machines +```````````````````````````````````````````````````````````````` + +.. cmd:: Register Inline @qualid + + This command gives as a hint to the reduction machines (VM and native) that + the body of the constant :n:`@qualid` should be inlined in the generated code. + +Registering primitive operations +```````````````````````````````` + +.. cmd:: Primitive @ident__1 := #@ident__2. + + Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When + running this command, the type of the primitive should be already known by + the kernel (this is achieved through this command for primitive types and + through the :cmd:`Register` command with the :g:`kernel` name-space for other + types). diff --git a/doc/stdlib/dune b/doc/stdlib/dune new file mode 100644 index 0000000000..7fe2493fbf --- /dev/null +++ b/doc/stdlib/dune @@ -0,0 +1,36 @@ +; This is an ad-hoc rule to ease the migration, it should be handled +; natively by Dune in the future. +(rule + (targets index-list.html) + (deps + make-library-index index-list.html.template hidden-files + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins)) + (action + (chdir %{project_root} + ; On windows run will fail + (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files")))) + +(rule + (targets html) + (deps + ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins) + (:header %{project_root}/doc/common/styles/html/coqremote/header.html) + (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) + ; For .glob files, should be gone when Coq Dune is smarter. + (package coq)) + (action + (progn + (run mkdir -p html) + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (run mv html/index.html html/genindex.html) + (with-stdout-to + _index.html + (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) + (run cp _index.html html/index.html)))) + +(alias + (name stdlib-html) + (deps html)) 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/coqide.ml b/ide/coqide.ml index 48c08899e0..94778e0c60 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1182,10 +1182,10 @@ let build_ui () = item "Help" ~label:"_Help"; item "Browse Coq Manual" ~label:"Browse Coq _Manual" ~callback:(fun _ -> - browse notebook#current_term.messages#default_route#add_string (doc_url ())); + browse notebook#current_term.messages#default_route#add_string Coq_config.wwwrefman); item "Browse Coq Library" ~label:"Browse Coq _Library" ~callback:(fun _ -> - browse notebook#current_term.messages#default_route#add_string library_url#get); + browse notebook#current_term.messages#default_route#add_string Coq_config.wwwstdlib); item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> browse_keyword sn.messages#default_route#add_string (get_current_word sn))); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c14af7d21d..5beaba3604 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -458,15 +458,6 @@ let browse prerr url = in run_command (fun _ -> ()) finally com -let doc_url () = - if doc_url#get = use_default_doc_url || doc_url#get = "" - then - let addr = List.fold_left Filename.concat (Envars.docdir ()) - ["html";"refman";"index.html"] - in - if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman - else doc_url#get - let url_for_keyword = let ht = Hashtbl.create 97 in lazy ( @@ -476,13 +467,7 @@ let url_for_keyword = (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt")) (Minilib.coqide_data_dirs ())) "index_urls.txt" in open_in index_urls - with Not_found -> - let doc_url = doc_url () in - let n = String.length doc_url in - if n > 8 && String.sub doc_url 0 7 = "file://" then - open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") - else - raise Exit + with Not_found -> raise Exit in try while true do let s = input_line cin in @@ -503,7 +488,7 @@ let url_for_keyword = let browse_keyword prerr text = try let u = Lazy.force url_for_keyword text in - browse prerr (doc_url() ^ u) + browse prerr (Coq_config.wwwrefman ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") let rec is_valid (s : Pp.t) = match Pp.repr s with diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 0031c59c17..531c71cd4b 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -13,7 +13,6 @@ val warning : string -> unit val cb : GData.clipboard -val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit diff --git a/ide/preferences.ml b/ide/preferences.ml index 4aa8c92f73..fb0eea1405 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -366,33 +366,6 @@ let text_font = in new preference ~name:["text_font"] ~init ~repr:Repr.(string) -let is_standard_doc_url url = - let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in - let n = String.length Coq_config.wwwcoq in - let n' = String.length Coq_config.wwwrefman in - url = Coq_config.localwwwrefman || - url = Coq_config.wwwrefman || - url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) - -let doc_url = -object - inherit [string] preference - ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) - as super - - method! set v = - if not (is_standard_doc_url v) && - v <> use_default_doc_url && - (* Extra hack to support links to last released doc version *) - v <> Coq_config.wwwcoq ^ "doc" && - v <> Coq_config.wwwcoq ^ "doc/" - then super#set v - -end - -let library_url = - new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string) - let show_toolbar = new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool) @@ -692,7 +665,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 @@ -948,32 +921,6 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in - let doc_url = - let predefined = [ - "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]); - Coq_config.wwwrefman; - use_default_doc_url - ] in - combo - "Manual URL" - ~f:doc_url#set - ~new_allowed: true - (predefined@[if List.mem doc_url#get predefined then "" - else doc_url#get]) - doc_url#get in - let library_url = - let predefined = [ - "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]); - Coq_config.wwwstdlib - ] in - combo - "Library URL" - ~f:(fun s -> library_url#set s) - ~new_allowed: true - (predefined@[if List.mem library_url#get predefined then "" - else library_url#get]) - library_url#get - in let automatic_tactics = strings ~f:automatic_tactics#set @@ -1039,7 +986,7 @@ let configure ?(apply=(fun () -> ())) parent = Section("Appearance", Some `PREFERENCES, [window_width; window_height]); Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; - cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); + cmd_print;cmd_editor;cmd_browse]); Section("Tactics Wizard", None, [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, diff --git a/ide/preferences.mli b/ide/preferences.mli index 7ed6a40bdb..cf2265781c 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -74,8 +74,6 @@ val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference val text_font : string preference -val doc_url : string preference -val library_url : string preference val show_toolbar : bool preference val contextual_menus_on_goal : bool preference val window_width : int preference 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/pretyping/cases.ml b/pretyping/cases.ml index ed7c3d6770..1ad90b2953 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -426,7 +426,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in (match find_row_ind tm1 with | None -> sigma, (current, tmtyp) - | Some (_,(ind,_)) -> + | Some (loc,(ind,_)) -> let sigma, indt = inductive_template !!(pb.env) sigma None ind in let sigma, current = if List.is_empty deps && isEvar sigma typ then @@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | None -> sigma, current | Some sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) 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. |