aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/PULL_REQUEST_TEMPLATE.md2
-rw-r--r--META.coq3
-rw-r--r--Makefile.build6
-rw-r--r--Makefile.ide1
-rw-r--r--checker/closure.ml18
-rw-r--r--checker/closure.mli5
-rw-r--r--checker/reduction.ml8
-rw-r--r--checker/subtyping.ml13
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh5
-rw-r--r--test-suite/coqchk/univ.v33
10 files changed, 66 insertions, 28 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index a9230042a5..86c15f6e80 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -12,5 +12,5 @@ Fixes / closes #????
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
-- [ ] Corresponding documentation was added / updated.
+- [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
- [ ] Entry added in CHANGES.
diff --git a/META.coq b/META.coq
index 12d7666cb0..8d4c3d5f00 100644
--- a/META.coq
+++ b/META.coq
@@ -57,9 +57,6 @@ package "vm" (
# We currently prefer static linking of the VM.
archive(byte) = "libcoqrun.a"
linkopts(byte) = "-custom"
-
- linkopts(native) = "-cclib -lcoqrun"
-
)
package "kernel" (
diff --git a/Makefile.build b/Makefile.build
index 1326027caa..7454e1b0c0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -397,7 +397,6 @@ $(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
- -I kernel/byterun/ -cclib -lcoqrun \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP) $@
@@ -637,6 +636,11 @@ kernel/kernel.cma: kernel/kernel.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+# Specific rule for kernel.cmxa as to adjoin -cclib -lcoqrun
+kernel/kernel.cmxa: kernel/kernel.mllib
+ $(SHOW)'OCAMLOPT -a -o $@'
+ $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^)
+
%.cma: %.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
diff --git a/Makefile.ide b/Makefile.ide
index 37f698e0c9..48b5549120 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -147,7 +147,6 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \
- -I kernel/byterun/ -cclib -lcoqrun \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP) $@
diff --git a/checker/closure.ml b/checker/closure.ml
index bfba6c161d..66e69f2250 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -135,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
* instantiations (cbv or lazy) are.
*)
-type 'a tableKey =
- | ConstKey of 'a
- | VarKey of Id.t
- | RelKey of int
-
type table_key = Constant.t puniverses tableKey
+
+let eq_pconstant_key (c,u) (c',u') =
+ eq_constant_key c c' && Univ.Instance.equal u u'
+
module KeyHash =
struct
type t = table_key
- let equal k1 k2 = match k1, k2 with
- | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2
- && Univ.Instance.equal u1 u2
- | VarKey id1, VarKey id2 -> Id.equal id1 id2
- | RelKey i1, RelKey i2 -> Int.equal i1 i2
- | (ConstKey _ | VarKey _ | RelKey _), _ -> false
+ let equal = Names.eq_table_key eq_pconstant_key
open Hashset.Combine
@@ -201,8 +195,6 @@ let defined_rels flags env =
let mind_equiv_infos info = mind_equiv info.i_env
-let eq_table_key = KeyHash.equal
-
let create mk_cl flgs env =
{ i_flags = flgs;
i_repr = mk_cl;
diff --git a/checker/closure.mli b/checker/closure.mli
index 4cf02ae2b0..49b07f730d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -58,10 +58,6 @@ val betaiotazeta : reds
val betadeltaiotanolet : reds
(***********************************************************************)
-type 'a tableKey =
- | ConstKey of 'a
- | VarKey of Id.t
- | RelKey of int
type table_key = Constant.t puniverses tableKey
@@ -162,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
(* [mind_equiv] checks whether two inductive types are intentionally equal *)
val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
-val eq_table_key : table_key -> table_key -> bool
(************************************************************************)
(*i This is for lazy debug *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 072dec63f1..4e508dc772 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open CErrors
open Util
open Cic
@@ -297,6 +298,11 @@ let oracle_order infos l2r k1 k2 =
if Int.equal n1 n2 then l2r
else n1 < n2
+let eq_table_key univ =
+ Names.eq_table_key (fun (c1,u1) (c2,u2) ->
+ Constant.UserOrd.equal c1 c2 &&
+ Univ.Instance.check_eq univ u1 u2)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -343,7 +349,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if eq_table_key fl1 fl2
+ if eq_table_key univ fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5cb38cb817..5c672d04a6 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -303,7 +303,18 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
| Constant cb1 ->
let cb1 = subst_const_body subst1 cb1 in
let cb2 = subst_const_body subst2 cb2 in
- (*Start by checking types*)
+ (*Start by checking universes *)
+ let env =
+ match cb1.const_universes, cb2.const_universes with
+ | Monomorphic_const _, Monomorphic_const _ -> env
+ | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
+ check_polymorphic_instance error env auctx1 auctx2
+ | Monomorphic_const _, Polymorphic_const _ ->
+ error ()
+ | Polymorphic_const _, Monomorphic_const _ ->
+ error ()
+ in
+ (* Now check types *)
let typ1 = cb1.const_type in
let typ2 = cb2.const_type in
check_type env typ1 typ2;
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5d96c24991..feabf72d48 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,5 +9,6 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
-fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
+fiat_crypto_CI_TARGETS1="printlite lite lite-display"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} )
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 19eea94b19..43815b61ea 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -46,3 +46,36 @@ Inductive constraint4 : (Type -> Type) -> Type
:= mk_constraint4 : let U1 := Type in
let U2 := Type in
constraint4 (fun x : U1 => (x : U2)).
+
+Module CMP_CON.
+ (* Comparison of opaque constants MUST be up to the universe graph.
+ See #6798. *)
+ Universe big.
+
+ Polymorphic Lemma foo@{u} : Type@{big}.
+ Proof. exact Type@{u}. Qed.
+
+ Universes U V.
+
+ Definition yo : foo@{U} = foo@{V} := eq_refl.
+End CMP_CON.
+
+Set Universe Polymorphism.
+
+Module POLY_SUBTYP.
+
+ Module Type T.
+ Axiom foo : Type.
+ Parameter bar@{u v|u = v} : foo@{u}.
+ End T.
+
+ Module M.
+ Axiom foo : Type.
+ Axiom bar@{u v|u = v} : foo@{v}.
+ End M.
+
+ Module F (A:T). End F.
+
+ Module X := F M.
+
+End POLY_SUBTYP.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:11:47 +0000