diff options
| -rw-r--r-- | pretyping/evarconv.ml | 6 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9971.v | 27 |
3 files changed, 30 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 00d4c7b3d8..16be4812fe 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -253,10 +253,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = (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 (proji, Const_cs c2), 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 @@ -273,6 +270,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..f26f59d6c5 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -179,10 +179,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) -> Const_cs (GlobRef.ConstRef (Projection.constant p)), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] 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. |