aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh9
-rw-r--r--doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst6
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
-rw-r--r--pretyping/evarconv.ml15
-rw-r--r--pretyping/recordops.ml22
-rw-r--r--pretyping/recordops.mli3
-rw-r--r--test-suite/bugs/closed/bug_9971.v27
7 files changed, 62 insertions, 22 deletions
diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh
new file mode 100644
index 0000000000..95f0de2bd3
--- /dev/null
+++ b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then
+
+ unicoq_CI_REF=master+adapting-coq-pr13386
+ unicoq_CI_GITURL=https://github.com/herbelin/unicoq
+
+ elpi_CI_REF=coq-master+adapting-coq-pr13386
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst
new file mode 100644
index 0000000000..4bd214d7be
--- /dev/null
+++ b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+ issue when two expressions involving different projections and one is
+ primitive need to be unified
+ (`#13386 <https://github.com/coq/coq/pull/13386>`_,
+ fixes `#9971 <https://github.com/coq/coq/issues/9971>`_,
+ by Hugo Herbelin).
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bd514f15d5..a4aa08300d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u =
let nb_cs_proj_args pc f u =
let na k =
- List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in
+ List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
let nargs_of_proj t = match kind t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 00d4c7b3d8..cdf2922516 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
Prod (_,a,b) -> (* assert (l2=[]); *)
let _, a, b = destProd sigma t2 in
if noccurn sigma 1 b then
- lookup_canonical_conversion (proji, Prod_cs),
+ lookup_canonical_conversion env (proji, Prod_cs),
(Stack.append_app [|a;pop b|] Stack.empty)
else raise Not_found
| Sort s ->
let s = ESorts.kind sigma s in
- lookup_canonical_conversion
+ lookup_canonical_conversion env
(proji, Sort_cs (Sorts.family s)),[]
| Proj (p, c) ->
- let c2 = GlobRef.ConstRef (Projection.constant p) in
- let c = Retyping.expand_projection env sigma p c [] in
- let _, args = destApp sigma c in
- let sk2 = Stack.append_app args sk2 in
- lookup_canonical_conversion (proji, Const_cs c2), sk2
+ lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2
| _ ->
let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
- lookup_canonical_conversion (proji, Const_cs c2),sk2
+ lookup_canonical_conversion env (proji, Const_cs c2),sk2
with Not_found ->
- let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
+ let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in
(c,cs),[]
in
let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
@@ -273,6 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
| Some c -> (* A primitive projection applied to c *)
let ty = Retyping.get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
+ (* Are we sure that ty is not an evar? *)
try Inductiveops.find_mrectype env sigma ty
with _ -> raise Not_found
in Stack.append_app_list ind_args Stack.empty, c, sk1
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6e5ad8dd4..b6e44265ae 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -144,19 +144,21 @@ type obj_typ = {
type cs_pattern =
Const_cs of GlobRef.t
+ | Proj_cs of Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
-let eq_cs_pattern p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2
+let eq_cs_pattern env p1 p2 = match p1, p2 with
+| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
| Prod_cs, Prod_cs -> true
| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
| Default_cs, Default_cs -> true
| _ -> false
-let rec assoc_pat a = function
- | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs
+let rec assoc_pat env a = function
+ | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs
| [] -> raise Not_found
@@ -179,10 +181,7 @@ let rec cs_pattern_of_constr env t =
patt, n, args @ Array.to_list vargs
| Rel n -> Default_cs, Some n, []
| Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
- | Proj (p, c) ->
- let ty = Retyping.get_type_of_constr env c in
- let _, params = Inductive.find_rectype env ty in
- Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
+ | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
| _ -> Const_cs (fst @@ destRef t) , None, []
@@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
let pr_cs_pattern = function
Const_cs c -> Nametab.pr_global_env Id.Set.empty c
+ | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p))
| Prod_cs -> str "_ -> _"
| Default_cs -> str "_"
| Sort_cs s -> Sorts.pr_sort_family s
@@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o =
compute_canonical_projections env ~warn o |>
List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
- match assoc_pat cs_pat l with
+ match assoc_pat env cs_pat l with
| exception Not_found ->
object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
| _, cs ->
@@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref =
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
(ref,indsp)
-let lookup_canonical_conversion (proj,pat) =
- assoc_pat pat (GlobRef.Map.find proj !object_table)
+let lookup_canonical_conversion env (proj,pat) =
+ assoc_pat env pat (GlobRef.Map.find proj !object_table)
let decompose_projection sigma c args =
match EConstr.kind sigma c with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3be60d5e62..5b8dc8184a 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option
(** A cs_pattern characterizes the form of a component of canonical structure *)
type cs_pattern =
Const_cs of GlobRef.t
+ | Proj_cs of Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
@@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t
type cs = GlobRef.t * inductive
-val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
+val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
cs -> unit
val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v
new file mode 100644
index 0000000000..ef526dcd7d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9971.v
@@ -0,0 +1,27 @@
+(* Test that it raises a normal error and not an anomaly *)
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
+Arguments pair {A B} _ _.
+Record piis := { dep_types : Type; indep_args : dep_types -> Type }.
+Import EqNotations.
+Goal forall (id : Set) (V : id) (piiio : id -> piis)
+ (Z : {ridc : id & prod (dep_types (piiio ridc)) True})
+ (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}),
+ let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in
+ prod True (ida V (projT1 W)) ->
+ Z = existT _ V (pair (projT1 W) I) ->
+ ida (projT1 Z) (fst (projT2 Z)).
+ intros.
+ refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+ H in
+ let v := I in
+ _);
+ refine (snd X).
+ Undo.
+Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+ H in
+ let v := I in
+ snd X).
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:10:47 +0000