aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/01-kernel/13356-primarray-cumul.rst5
-rw-r--r--doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst5
-rw-r--r--doc/sphinx/addendum/type-classes.rst13
-rw-r--r--doc/sphinx/language/core/definitions.rst21
-rw-r--r--doc/sphinx/language/extensions/match.rst7
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst20
-rw-r--r--doc/tools/docgram/common.edit_mlg7
-rw-r--r--doc/tools/docgram/orderedGrammar28
-rw-r--r--engine/eConstr.ml3
-rw-r--r--engine/evarutil.ml3
-rw-r--r--kernel/cClosure.ml8
-rw-r--r--kernel/environ.ml6
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/nativecode.ml75
-rw-r--r--kernel/nativecode.mli1
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/reduction.ml49
-rw-r--r--plugins/ltac/g_ltac.mlg8
-rw-r--r--pretyping/evarconv.ml9
-rw-r--r--test-suite/bugs/closed/bug_13348.v10
-rw-r--r--test-suite/bugs/closed/bug_13354.v10
-rw-r--r--test-suite/success/proof_using_noinit.v9
-rw-r--r--vernac/g_proofs.mlg2
-rw-r--r--vernac/g_vernac.mlg3
24 files changed, 186 insertions, 121 deletions
diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst
new file mode 100644
index 0000000000..978ca325bf
--- /dev/null
+++ b/doc/changelog/01-kernel/13356-primarray-cumul.rst
@@ -0,0 +1,5 @@
+- **Changed:** Primitive arrays are now irrelevant in their single
+ polymorphic universe (same as a polymorphic cumulative list
+ inductive would be) (`#13356
+ <https://github.com/coq/coq/pull/13356>`_, fixes `#13354
+ <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst
new file mode 100644
index 0000000000..9ae759be56
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ The :cmd:`Proof using` command can now be used without loading the
+ Ltac plugin (`-noinit` mode)
+ (`#13339 <https://github.com/coq/coq/pull/13339>`_,
+ by Théo Zimmermann).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index cdd31fcb86..56d90b33d8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -336,20 +336,23 @@ Summary of the commands
.. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } }
- .. insertprodn hint_info hint_info
+ .. insertprodn hint_info one_pattern
.. prodn::
- hint_info ::= %| {? @natural } {? @one_term }
+ hint_info ::= %| {? @natural } {? @one_pattern }
+ one_pattern ::= @one_term
Declares a typeclass instance named
:token:`ident_decl` of the class :n:`@type` with the specified parameters and with
fields defined by :token:`field_def`, where each field must be a declared field of
the class.
- Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
- specifies the hint priority, where 0 is the highest priority as for
+ Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
+ may be used to specify the hint priority, where 0 is the highest priority as for
:tacn:`auto` hints. If the priority is not specified, the default is the number
- of non-dependent binders of the instance.
+ of non-dependent binders of the instance. If :token:`one_pattern` is given, terms
+ matching that pattern will trigger use of the instance. Otherwise,
+ use is triggered based on the conclusion of the type.
This command supports the :attr:`global` attribute that can be
used on instances declared in a section so that their
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 4ea3ea5e6d..79489c85f6 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -13,15 +13,18 @@ Let-in definitions
.. prodn::
term_let ::= let @name {? : @type } := @term in @term
| let @name {+ @binder } {? : @type } := @term in @term
- | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
- | let ' @pattern := @term {? return @term100 } in @term
- | let ' @pattern in @pattern := @term return @term100 in @term
-
-:n:`let @ident := @term in @term’`
-denotes the local binding of :n:`@term` to the variable
-:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in
-definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
-stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
+ | @destructuring_let
+
+:n:`let @ident := @term__1 in @term__2` represents the local binding of
+the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`.
+
+:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation
+for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`.
+
+.. seealso::
+
+ Extensions of the `let ... in ...` syntax are described in
+ :ref:`irrefutable-patterns`.
.. index::
single: ... : ... (type cast)
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 23389eba3b..8e62c2af13 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one
constructor can be alternatively written using :g:`let … in …`
constructions. There are two variants of them.
+.. insertprodn destructuring_let destructuring_let
+
+.. prodn::
+ destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
+ | let ' @pattern := @term {? return @term100 } in @term
+ | let ' @pattern in @pattern := @term return @term100 in @term
+
First destructuring let syntax
++++++++++++++++++++++++++++++
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7baf193266..86d1d25745 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -133,7 +133,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
.. prodn::
search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key }
- | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term
+ | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern
| is : @logical_kind
Searched objects can be filtered by patterns, by the constants they
@@ -141,9 +141,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
names.
The location of the pattern or constant within a term
- :n:`@one_term`
+ :n:`@one_pattern`
Search for objects whose type contains a subterm matching the
- pattern :n:`@one_term`. Holes of the pattern are indicated by
+ pattern :n:`@one_pattern`. Holes of the pattern are indicated by
`_` or :n:`?@ident`. If the same :n:`?@ident` occurs more than
once in the pattern, all occurrences in the subterm must be
identical. See :ref:`this example <search-pattern>`.
@@ -312,7 +312,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
Search is:Instance [ Reflexive | Symmetric ].
-.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } }
.. deprecated:: 8.12
@@ -320,8 +320,8 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context that have the
- form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term`
- matches a subterm of `C` in head position. For example, a :n:`@one_term` of `f _ b`
+ form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern`
+ matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b`
matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
@@ -337,12 +337,12 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
SearchHead le.
SearchHead (@eq bool).
-.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } }
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context
ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern
- :n:`@one_term`.
+ :n:`@one_pattern`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
@@ -362,11 +362,11 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
SearchPattern (?X1 + _ = _ + ?X1).
-.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } }
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context that have the form
- :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term`
+ :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern`
matches either `LHS` or `RHS`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4ad32e15eb..4c1956d172 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -285,9 +285,12 @@ term_let: [
(* Don't need to document that "( )" is equivalent to "()" *)
| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
| REPLACE "let" "'" pattern200 ":=" term200 "in" term200
-| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
]
atomic_constr: [
@@ -2478,7 +2481,6 @@ SPLICE: [
| binders
| casted_constr
| check_module_types
-| constr_pattern
| decl_sep
| function_fix_definition (* loses funind annotation *)
| glob
@@ -2652,6 +2654,7 @@ RENAME: [
| ssrfwd ssrdefbody
| ssrclauses ssr_in
| ssrcpat ssrblockpat
+| constr_pattern one_pattern
]
simple_tactic: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c697043f27..26474d950a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -473,6 +473,10 @@ ssr_dpat: [
term_let: [
| "let" name OPT ( ":" type ) ":=" term "in" term
| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
+| destructuring_let
+]
+
+destructuring_let: [
| "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
| "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
| "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
@@ -724,7 +728,11 @@ sort_family: [
]
hint_info: [
-| "|" OPT natural OPT one_term
+| "|" OPT natural OPT one_pattern
+]
+
+one_pattern: [
+| one_term
]
module_binder: [
@@ -1011,7 +1019,7 @@ command: [
| "Prenex" "Implicits" LIST1 qualid (* SSR plugin *)
| "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *)
| "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *)
-| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *)
+| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *)
| "Typeclasses" "Transparent" LIST1 qualid
| "Typeclasses" "Opaque" LIST1 qualid
| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
@@ -1107,9 +1115,9 @@ command: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
@@ -1167,7 +1175,7 @@ search_query: [
search_item: [
| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
-| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern
| "is" ":" logical_kind
]
@@ -1196,7 +1204,7 @@ hint: [
| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
| "Unfold" LIST1 qualid
| "Constructors" LIST1 qualid
-| "Extern" natural OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_pattern "=>" ltac_expr
]
tacdef_body: [
@@ -2404,9 +2412,9 @@ tac2mode: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
]
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0c84dee572..c29de27efb 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -452,6 +452,9 @@ let eq_universes env sigma cstrs cv_pb refargs l l' =
let open GlobRef in
let open UnivProblem in
match refargs with
+ | Some (ConstRef c, 1) when Environ.is_array_type env c ->
+ cstrs := compare_cumulative_instances cv_pb true [|Univ.Variance.Irrelevant|] l l' !cstrs;
+ true
| None | Some (ConstRef _, _) ->
cstrs := enforce_eq_instances_univs true l l' !cstrs; true
| Some (VarRef _, _) -> assert false (* variables don't have instances *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 771571fd3f..ba6a9ea6d9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -371,7 +371,8 @@ let push_rel_decl_to_named_context
let subst = update_var id0 id subst in
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
let nc = replace_var_named_declaration id0 id nc in
- (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc)
+ let avoid = Id.Set.add id (Id.Set.add id0 avoid) in
+ (push_var id0 subst, avoid, push_named_context_val d nc)
| Some id0 when hypnaming = FailIfConflict ->
user_err Pp.(Id.print id0 ++ str " is already used.")
| _ ->
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 174125fc57..17feeb9b5a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1098,14 +1098,8 @@ module FNativeEntries =
let defined_array = ref false
- let farray = ref dummy
-
let init_array retro =
- match retro.Retroknowledge.retro_array with
- | Some c ->
- defined_array := true;
- farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
- | None -> defined_array := false
+ defined_array := Option.has_some retro.Retroknowledge.retro_array
let init env =
current_retro := env.retroknowledge;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 914c951eb6..69edb1498c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref
type link_info =
| Linked of string
- | LinkedInteractive of string
| NotLinked
type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
@@ -569,6 +568,11 @@ let is_primitive env c =
| Declarations.Primitive _ -> true
| _ -> false
+let is_array_type env c =
+ match env.retroknowledge.Retroknowledge.retro_array with
+ | None -> false
+ | Some c' -> Constant.CanOrd.equal c c'
+
let polymorphic_constant cst env =
Declareops.constant_is_polymorphic (lookup_constant cst env)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60696184ef..6a8ddce835 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val
(** Linking information for the native compiler *)
type link_info =
| Linked of string
- | LinkedInteractive of string
| NotLinked
type key = int CEphemeron.key option ref
@@ -250,6 +249,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
val is_primitive : env -> Constant.t -> bool
+val is_array_type : env -> Constant.t -> bool
+
(** {6 Primitive projections} *)
(** Checks that the number of parameters is correct. *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 911a879394..09db29d222 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1933,7 +1933,7 @@ and compile_named env sigma univ auxdefs id =
| LocalAssum _ ->
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
-let compile_constant env sigma prefix ~interactive con cb =
+let compile_constant env sigma con cb =
let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
begin match cb.const_body with
| Def t ->
@@ -1942,10 +1942,6 @@ let compile_constant env sigma prefix ~interactive con cb =
if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
let is_lazy = is_lazy t in
let code = if is_lazy then mk_lazy code else code in
- let name =
- if interactive then LinkedInteractive prefix
- else Linked prefix
- in
let l = Constant.label con in
let auxdefs,code =
if no_univs then compile_with_fv env sigma None [] (Some l) code
@@ -1959,7 +1955,7 @@ let compile_constant env sigma prefix ~interactive con cb =
optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
in
if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
- code, name
+ code
| _ ->
let i = push_symbol (SymbConst con) in
let args =
@@ -1969,9 +1965,7 @@ let compile_constant env sigma prefix ~interactive con cb =
(*
let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
*)
- [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)],
- if interactive then LinkedInteractive prefix
- else Linked prefix
+ [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)]
end
module StringOrd = struct type t = string let compare = String.compare end
@@ -1984,12 +1978,9 @@ let is_loaded_native_file s = StringSet.mem s !loaded_native_files
let register_native_file s =
loaded_native_files := StringSet.add s !loaded_native_files
-let is_code_loaded ~interactive name =
+let is_code_loaded name =
match !name with
| NotLinked -> false
- | LinkedInteractive s ->
- if (interactive && is_loaded_native_file s) then true
- else (name := NotLinked; false)
| Linked s ->
if is_loaded_native_file s then true
else (name := NotLinked; false)
@@ -2049,8 +2040,11 @@ let compile_mind mb mind stack =
in
Array.fold_left_i f stack mb.mind_packets
-type code_location_update =
- link_info ref * link_info
+type code_location_update = {
+ upd_info : link_info ref;
+ upd_prefix : string;
+}
+
type code_location_updates =
code_location_update Mindmap_env.t * code_location_update Cmap_env.t
@@ -2058,35 +2052,34 @@ type linkable_code = global list * code_location_updates
let empty_updates = Mindmap_env.empty, Cmap_env.empty
-let compile_mind_deps env prefix ~interactive
+let compile_mind_deps env prefix
(comp_stack, (mind_updates, const_updates) as init) mind =
let mib,nameref = lookup_mind_key mind env in
- if is_code_loaded ~interactive nameref
+ if is_code_loaded nameref
|| Mindmap_env.mem mind mind_updates
then init
else
let comp_stack =
compile_mind mib mind comp_stack
in
- let name =
- if interactive then LinkedInteractive prefix
- else Linked prefix
- in
- let upd = (nameref, name) in
+ let upd = {
+ upd_info = nameref;
+ upd_prefix = prefix;
+ } in
let mind_updates = Mindmap_env.add mind upd mind_updates in
(comp_stack, (mind_updates, const_updates))
(* This function compiles all necessary dependencies of t, and generates code in
reverse order, as well as linking information updates *)
-let compile_deps env sigma prefix ~interactive init t =
+let compile_deps env sigma prefix init t =
let rec aux env lvl init t =
match kind t with
- | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind
+ | Ind ((mind,_),_u) -> compile_mind_deps env prefix init mind
| Const c ->
let c,_u = get_alias env c in
let cb,(nameref,_) = lookup_constant_key c env in
let (_, (_, const_updates)) = init in
- if is_code_loaded ~interactive nameref
+ if is_code_loaded nameref
|| (Cmap_env.mem c const_updates)
then init
else
@@ -2096,19 +2089,21 @@ let compile_deps env sigma prefix ~interactive init t =
aux env lvl init (Mod_subst.force_constr t)
| _ -> init
in
- let code, name =
- compile_constant env sigma prefix ~interactive c cb
- in
+ let code = compile_constant env sigma c cb in
+ let upd = {
+ upd_info = nameref;
+ upd_prefix = prefix;
+ } in
let comp_stack = code@comp_stack in
- let const_updates = Cmap_env.add c (nameref, name) const_updates in
+ let const_updates = Cmap_env.add c upd const_updates in
comp_stack, (mind_updates, const_updates)
- | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind
+ | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix init mind
| Proj (p,c) ->
- let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
+ let init = compile_mind_deps env prefix init (Projection.mind p) in
aux env lvl init c
| Case (ci, _p, _iv, _c, _ac) ->
let mind = fst ci.ci_ind in
- let init = compile_mind_deps env prefix ~interactive init mind in
+ let init = compile_mind_deps env prefix init mind in
fold_constr_with_binders succ (aux env) lvl init t
| Var id ->
let open Context.Named.Declaration in
@@ -2130,11 +2125,8 @@ let compile_deps env sigma prefix ~interactive init t =
in
aux env 0 init t
-let compile_constant_field env prefix con acc cb =
- let (gl, _) =
- compile_constant ~interactive:false env empty_evars prefix
- con cb
- in
+let compile_constant_field env _prefix con acc cb =
+ let gl = compile_constant env empty_evars con cb in
gl@acc
let compile_mind_field mp l acc mb =
@@ -2152,11 +2144,11 @@ let mk_conv_code env sigma prefix t1 t2 =
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env sigma prefix ~interactive:true init t1
+ compile_deps env sigma prefix init t1
in
let gl, (mind_updates, const_updates) =
let init = (gl, (mind_updates, const_updates)) in
- compile_deps env sigma prefix ~interactive:true init t2
+ compile_deps env sigma prefix init t2
in
let code1 = lambda_of_constr env sigma t1 in
let code2 = lambda_of_constr env sigma t2 in
@@ -2179,7 +2171,7 @@ let mk_norm_code env sigma prefix t =
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env sigma prefix ~interactive:true init t
+ compile_deps env sigma prefix init t
in
let code = lambda_of_constr env sigma t in
let (gl,code) = compile_with_fv env sigma None gl None code in
@@ -2196,7 +2188,8 @@ let mk_library_header (symbols : Nativevalues.symbols) =
let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in
[Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
-let update_location (r,v) = r := v
+let update_location r =
+ r.upd_info := Linked r.upd_prefix
let update_locations (ind_updates,const_updates) =
Mindmap_env.iter (fun _ -> update_location) ind_updates;
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 913b3843c2..aab6e1d4a0 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -50,7 +50,6 @@ val get_proj : symbols -> int -> inductive * int
val get_symbols : unit -> symbols
-type code_location_update
type code_location_updates
type linkable_code = global list * code_location_updates
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index e98e97907a..18f16f427d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -111,14 +111,12 @@ let get_mind_prefix env mind =
match !name with
| NotLinked -> ""
| Linked s -> s
- | LinkedInteractive s -> s
let get_const_prefix env c =
let _,(nameref,_) = lookup_constant_key c env in
match !nameref with
| NotLinked -> ""
| Linked s -> s
- | LinkedInteractive s -> s
(* A generic map function *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c891b885c4..cf40263f61 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -280,11 +280,12 @@ let convert_constructors ctor nargs u1 u2 (s, check) =
convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
ctor nargs u1 u2 s, check
-let conv_table_key infos k1 k2 cuniv =
+let conv_table_key infos ~nargs k1 k2 cuniv =
if k1 == k2 then cuniv else
match k1, k2 with
| ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
if Univ.Instance.equal u u' then cuniv
+ else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv
else
let flex = evaluable_constant cst (info_env infos)
&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
@@ -304,6 +305,11 @@ let unfold_ref_with_args infos tab fl v =
Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v)))
| Undef _ | OpaqueDef _ | Primitive _ -> None
+let same_args_size sk1 sk2 =
+ let n = CClosure.stack_args_size sk1 in
+ if Int.equal n (CClosure.stack_args_size sk2) then n
+ else raise NotConvertible
+
type conv_tab = {
cnv_inf : clos_infos;
lft_tab : clos_tab;
@@ -408,7 +414,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
- let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
+ let nargs = same_args_size v1 v2 in
+ let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in
@@ -577,17 +584,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
- let nargs = CClosure.stack_args_size v1 in
- if not (Int.equal nargs (CClosure.stack_args_size v2))
- then raise NotConvertible
- else
- match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
- | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- | exception MustExpand ->
- let env = info_env infos.cnv_inf in
- let hd1 = eta_expand_ind env pind1 in
- let hd2 = eta_expand_ind env pind2 in
- eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+ let nargs = same_args_size v1 v2 in
+ match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_ind env pind1 in
+ let hd2 = eta_expand_ind env pind2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
| (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
@@ -597,17 +601,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
- let nargs = CClosure.stack_args_size v1 in
- if not (Int.equal nargs (CClosure.stack_args_size v2))
- then raise NotConvertible
- else
- match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
- | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
- | exception MustExpand ->
- let env = info_env infos.cnv_inf in
- let hd1 = eta_expand_constructor env pctor1 in
- let hd2 = eta_expand_constructor env pctor2 in
- eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+ let nargs = same_args_size v1 v2 in
+ match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_constructor env pctor1 in
+ let hd2 = eta_expand_constructor env pctor2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
(* Eta expansion of records *)
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c54f8ffa78..c2e95c45f9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -329,11 +329,11 @@ GRAMMAR EXTEND Gram
;
command:
[ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
- l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
+ l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
{ Vernacexpr.VernacProof (Some (in_tac ta), l) }
- | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
- ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
- { Vernacexpr.VernacProof (ta,Some l) } ] ]
+ | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
+ "with"; ta = Pltac.tactic ->
+ { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
;
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 90af143a2d..ca16c52026 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -567,8 +567,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
let compare_heads evd =
match EConstr.kind evd term, EConstr.kind evd term' with
| Const (c, u), Const (c', u') when QConstant.equal env c c' ->
- let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
- check_strict evd u u'
+ if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c
+ then
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ check_strict evd u u'
| Const _, Const _ -> UnifFailure (evd, NotSameHead)
| Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
if EInstance.is_empty u && EInstance.is_empty u' then Success evd
diff --git a/test-suite/bugs/closed/bug_13348.v b/test-suite/bugs/closed/bug_13348.v
new file mode 100644
index 0000000000..d3d5d3e5b4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13348.v
@@ -0,0 +1,10 @@
+Generalizable All Variables.
+
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
+Arguments populate {_} _.
+
+Set Mangle Names.
+Axioms _0 _1 _2 : Prop.
+
+Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B)
+ := populate (fun _ => inhabitant).
diff --git a/test-suite/bugs/closed/bug_13354.v b/test-suite/bugs/closed/bug_13354.v
new file mode 100644
index 0000000000..fbda10a9d2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13354.v
@@ -0,0 +1,10 @@
+
+Primitive array := #array_type.
+
+Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |].
+
+Definition on_array {A:Type} (x:array A) : Prop := True.
+
+Check on_array testArray.
+
+Check @on_array nat testArray.
diff --git a/test-suite/success/proof_using_noinit.v b/test-suite/success/proof_using_noinit.v
new file mode 100644
index 0000000000..f99b49619c
--- /dev/null
+++ b/test-suite/success/proof_using_noinit.v
@@ -0,0 +1,9 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
+Section A.
+Variable A : Prop.
+Hypothesis a : A.
+Lemma b : A.
+Proof using a.
+Admitted.
+End A.
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index ebec720ce2..5b80ed6794 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -56,6 +56,8 @@ GRAMMAR EXTEND Gram
[ [ IDENT "Goal"; c = lconstr ->
{ VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) }
| IDENT "Proof" -> { VernacProof (None,None) }
+ | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr ->
+ { VernacProof (None,Some l) }
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn }
| IDENT "Proof"; c = lconstr -> { VernacExactProof c }
| IDENT "Abort" -> { VernacAbort None }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f192d67624..1c80d71ea5 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -114,7 +114,8 @@ GRAMMAR EXTEND Gram
;
attribute:
[ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v }
- | "using" ; v = attr_value -> { "using", v } ]
+ (* Required because "ident" is declared a keyword when loading Ltac. *)
+ | IDENT "using" ; v = attr_value -> { "using", v } ]
]
;
attr_value:
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:48:04 +0000