aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES1
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/declarations.ml9
-rw-r--r--checker/values.ml4
-rwxr-xr-xdev/tools/merge-pr.sh18
-rwxr-xr-xdoc/sphinx/conf.py6
-rw-r--r--doc/sphinx/language/gallina-extensions.rst83
-rw-r--r--kernel/constr.ml16
-rw-r--r--kernel/constr.mli30
-rw-r--r--kernel/mod_subst.ml11
-rw-r--r--kernel/mod_subst.mli2
-rw-r--r--kernel/modops.ml3
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--test-suite/bugs/closed/2800.v13
-rw-r--r--test-suite/bugs/closed/7615.v19
-rw-r--r--test-suite/success/Hints.v2
17 files changed, 143 insertions, 81 deletions
diff --git a/CHANGES b/CHANGES
index 787c9ba12a..ce8e313b99 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,7 @@ Changes from 8.8.0 to 8.8.1
Kernel
- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with inlining of polymorphic constants (#7615).
Notations
diff --git a/checker/cic.mli b/checker/cic.mli
index 27e2a479f5..7ec3457686 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,7 +128,7 @@ type section_context = unit
(** {6 Substitutions} *)
type delta_hint =
- | Inline of int * constr option
+ | Inline of int * (Univ.AUContext.t * constr) option
| Equiv of KerName.t
type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
diff --git a/checker/declarations.ml b/checker/declarations.ml
index e1d2cf6d1d..a744a02279 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -196,7 +196,12 @@ let subst_con0 sub con u =
let dup con = con, Const (con, u) in
let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
match constant_of_delta_with_inline resolve con' with
- | Some t -> con', t
+ | Some (ctx, t) ->
+ (** FIXME: we never typecheck the inlined term, so that it could well
+ be garbage. What environment do we type it in though? The substitution
+ code should be moot in the checker but it **is** used nonetheless. *)
+ let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in
+ con', subst_instance_constr u t
| None ->
let con'' = match side with
| User -> constant_of_delta resolve con'
@@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver =
let kkey' = if dom then subst_kn subst kkey else kkey in
let hint' = match hint with
| Equiv kequ -> Equiv (subst_kn_delta subst kequ)
- | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/checker/values.ml b/checker/values.ml
index f7ab95fe2a..67032bd1b7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
+MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
*)
@@ -173,7 +173,7 @@ let v_section_ctxt = v_enum "emptylist" 1
(** kernel/mod_subst *)
let v_delta_hint =
- v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|]
+ v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
let v_resolver =
v_tuple "delta_resolver"
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 00d04e6b3d..320ef6ed07 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -140,6 +140,24 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then
fi
fi
+# Sanity check: PR has an outdated version of CI
+
+BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
+CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+
+if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+then
+ warning "This PR didn't run with the latest version of CI."
+ warning "It is probably a good idea to ask for a rebase."
+ read -p "Do you want to see the diff? [Y/n] " $QUICK_CONF -r
+ echo
+ if [[ ! $REPLY =~ ^[Nn]$ ]]
+ then
+ git diff "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
+ fi
+ ask_confirmation
+fi
+
# Sanity check: CI failed
STATUS=$(curl -s "$API/commits/$COMMIT/status")
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index f65400e88c..135c24aed9 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -201,9 +201,9 @@ html_static_path = ['_static']
# The empty string is equivalent to '%b %d, %Y'.
#html_last_updated_fmt = None
-# If true, SmartyPants will be used to convert quotes and dashes to
-# typographically correct entities.
-html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there
+# FIXME: this could be re-enabled after ensuring that smart quotes are locally
+# disabled for all relevant directives
+smartquotes = False
# Custom sidebar templates, maps document names to template names.
#html_sidebars = {}
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ff5d352c99..c21d8d4ec8 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1925,74 +1925,75 @@ applied to an unknown structure instance (an implicit argument) and a
value. The complete documentation of canonical structures can be found
in :ref:`canonicalstructures`; here only a simple example is given.
-Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the
-structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
-`qualid` is declared as a canonical structure using the command
-
.. cmd:: Canonical Structure @qualid
-Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
-solved during the type-checking process, `qualid` is used as a solution.
-Otherwise said, `qualid` is canonically used to extend the field |c_i|
-into a complete structure built on |c_i|.
+ This command declares :token:`qualid` as a canonical structure.
-Canonical structures are particularly useful when mixed with coercions
-and strict implicit arguments. Here is an example.
+ Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
+ structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
+ Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+ solved during the type-checking process, :token:`qualid` is used as a solution.
+ Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
+ into a complete structure built on |c_i|.
-.. coqtop:: all
+ Canonical structures are particularly useful when mixed with coercions
+ and strict implicit arguments.
- Require Import Relations.
+ .. example::
- Require Import EqNat.
+ Here is an example.
- Set Implicit Arguments.
+ .. coqtop:: all
- Unset Strict Implicit.
+ Require Import Relations.
- Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
- Prf_equiv : equivalence Carrier Equal}.
+ Require Import EqNat.
- Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+ Set Implicit Arguments.
- Axiom eq_nat_equiv : equivalence nat eq_nat.
+ Unset Strict Implicit.
- Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+ Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+ Prf_equiv : equivalence Carrier Equal}.
- Canonical Structure nat_setoid.
+ Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
-Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
-and ``B`` can be synthesized in the next statement.
+ Axiom eq_nat_equiv : equivalence nat eq_nat.
-.. coqtop:: all
+ Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
- Lemma is_law_S : is_law S.
+ Canonical Structure nat_setoid.
-Remark: If a same field occurs in several canonical structure, then
-only the structure declared first as canonical is considered.
+ Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A`
+ and :g:`B` can be synthesized in the next statement.
-.. cmdv:: Canonical Structure @ident := @term : @type
+ .. coqtop:: all
-.. cmdv:: Canonical Structure @ident := @term
+ Lemma is_law_S : is_law S.
-.. cmdv:: Canonical Structure @ident : @type := @term
+ .. note::
+ If a same field occurs in several canonical structures, then
+ only the structure declared first as canonical is considered.
-These are equivalent to a regular definition of `ident` followed by the declaration
-``Canonical Structure`` `ident`.
+ .. cmdv:: Canonical Structure @ident {? : @type } := @term
-See also: more examples in user contribution category (Rocq/ALGEBRA).
+ This is equivalent to a regular definition of :token:`ident` followed by the
+ declaration :n:`Canonical Structure @ident`.
-Print Canonical Projections.
-++++++++++++++++++++++++++++
+.. cmd:: Print Canonical Projections
-This displays the list of global names that are components of some
-canonical structure. For each of them, the canonical structure of
-which it is a projection is indicated. For instance, the above example
-gives the following output:
+ This displays the list of global names that are components of some
+ canonical structure. For each of them, the canonical structure of
+ which it is a projection is indicated.
-.. coqtop:: all
+ .. example::
+
+ For instance, the above example gives the following output:
+
+ .. coqtop:: all
- Print Canonical Projections.
+ Print Canonical Projections.
Implicit types of variables
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c11b9ebf46..4182293301 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term
type constr = t
type existential = existential_key * constr array
-type rec_declaration = Name.t array * constr array * constr array
-type fixpoint = (int array * int) * rec_declaration
- (* The array of [int]'s tells for each component of the array of
- mutual fixpoints the number of lambdas to skip before finding the
- recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
- (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
- the recursive argument);
- The second component [int] tells which component of the block is
- returned *)
-type cofixpoint = int * rec_declaration
- (* The component [int] tells which component of the block of
- cofixpoint is returned *)
type types = constr
+type rec_declaration = (constr, types) prec_declaration
+type fixpoint = (constr, types) pfixpoint
+type cofixpoint = (constr, types) pcofixpoint
+
(*********************)
(* Term constructors *)
(*********************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 742a13919a..bf7b5e87b5 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr
where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
+type ('constr, 'types) prec_declaration =
+ Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+ (int array * int) * ('constr, 'types) prec_declaration
+ (* The array of [int]'s tells for each component of the array of
+ mutual fixpoints the number of lambdas to skip before finding the
+ recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+ (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+ the recursive argument);
+ The second component [int] tells which component of the block is
+ returned *)
+
+type ('constr, 'types) pcofixpoint =
+ int * ('constr, 'types) prec_declaration
+ (* The component [int] tells which component of the block of
+ cofixpoint is returned *)
+
+type rec_declaration = (constr, types) prec_declaration
+
+type fixpoint = (constr, types) pfixpoint
val mkFix : fixpoint -> constr
(** If [funnames = [|f1,.....fn|]]
@@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr
...
with fn = bn.]
*)
-type cofixpoint = int * rec_declaration
+type cofixpoint = (constr, types) pcofixpoint
val mkCoFix : cofixpoint -> constr
@@ -185,12 +203,6 @@ val mkCoFix : cofixpoint -> constr
(** [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
type 'constr pexistential = Evar.t * 'constr array
-type ('constr, 'types) prec_declaration =
- Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
- (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
- int * ('constr, 'types) prec_declaration
type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 0027ebecfc..a47af56ca5 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -24,7 +24,7 @@ open Constr
is the term into which we should inline. *)
type delta_hint =
- | Inline of int * constr option
+ | Inline of int * (Univ.AUContext.t * constr) option
| Equiv of KerName.t
(* NB: earlier constructor Prefix_equiv of ModPath.t
@@ -158,7 +158,7 @@ let find_prefix resolve mp =
(** Applying a resolver to a kernel name *)
-exception Change_equiv_to_inline of (int * constr)
+exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr))
let solve_delta_kn resolve kn =
try
@@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) =
let knu = KerName.make mpu dir l in
let knc = if mpu == mpc then knu else KerName.make mpc dir l in
match search_delta_inline resolve knu knc with
- | Some t ->
+ | Some (ctx, t) ->
(* In case of inlining, discard the canonical part (cf #2608) *)
- Constant.make1 knu, t
+ let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in
+ Constant.make1 knu, Vars.subst_instance_constr u t
| None ->
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
@@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver =
| Equiv kequ ->
(try Equiv (subst_kn_delta subst kequ)
with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
- | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index b14d392073..76a1d173b9 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
KerName.t -> KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver :
- KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
+ KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2038171183..22f523a9ae 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
| Undef _ | OpaqueDef _ -> l
| Def body ->
let constr = Mod_subst.force_constr body in
- add_inline_delta_resolver kn (lev, Some constr) l
+ let ctx = Declareops.constant_polymorphic_context constant in
+ add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
with Not_found ->
error_no_such_label_sub (Constant.label con)
(ModPath.to_string (Constant.modpath con))
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8a8f9e71aa..04dd7d6e99 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1049,8 +1049,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
push_trace(loc,call) ist >>= fun trace ->
Profile_ltac.do_profile "eval_tactic:2" trace
(catch_error_tac trace (interp_atomic ist t))
- | TacFun _ | TacLetIn _ -> assert false
- | TacMatchGoal _ | TacMatch _ -> assert false
+ | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
let msgnl =
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 544175c6d2..ba4cde6d67 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -87,7 +87,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
let evd' =
if has_typeclass then
Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
- ~fail:(not with_evars) clenv.env clenv.evd
+ ~fail:(not with_evars) ~split:false clenv.env clenv.evd
else clenv.evd
in
if has_resolvable then
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee438934e..54c75e344c 100644
--- a/test-suite/bugs/closed/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -4,3 +4,16 @@ intuition
match goal with
| |- _ => idtac " foo"
end.
+
+ lazymatch goal with _ => idtac end.
+ match goal with _ => idtac end.
+ unshelve lazymatch goal with _ => idtac end.
+ unshelve match goal with _ => idtac end.
+ unshelve (let x := I in idtac).
+Abort.
+
+Require Import ssreflect.
+
+Goal True.
+match goal with _ => idtac end => //.
+Qed.
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 0000000000..cd8c4ad7df
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 8d08f5975e..717dc0debe 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -169,7 +169,7 @@ Proof.
Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
(a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
- Timeout 1 Fail apply _. (* 0.06s *)
+Timeout 1 Fail apply _. (* 0.06s *)
Abort.
End HintCut.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:06:19 +0000