diff options
-rw-r--r-- | pretyping/recordops.ml | 17 | ||||
-rw-r--r-- | test-suite/output/Warnings.out | 3 | ||||
-rw-r--r-- | test-suite/output/Warnings.v | 5 |
3 files changed, 18 insertions, 7 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 283a1dcd1..be43e9e1f 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -189,9 +189,14 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (t,con_pp,proji_sp_pp) -> + (fun (sign,env,t,con,proji_sp) -> + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in + let env = Termops.push_rels_assum sign env in + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in strbrk "Projection value has no head constant: " - ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " + ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) @@ -202,9 +207,9 @@ let compute_canonical_projections warn (con,ind) = let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in - let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in + let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in @@ -221,9 +226,7 @@ let compute_canonical_projections warn (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) - and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); l end | _ -> l) diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 000000000..a70f8ca45 --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 000000000..7465442ca --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + |