diff options
| author | Hugo Herbelin | 2020-11-15 10:28:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-19 20:43:42 +0100 |
| commit | a27fb3c67238cc41dc24308a233a02422e0f83f3 (patch) | |
| tree | 62ff07c1866494a1115c1e150356ac3db8ccc0a1 /pretyping/evarconv.ml | |
| parent | c7686fe3ddd90ea707411296bbc9ec0b8cc99a2c (diff) | |
Fixes #9971: expand_projections failing on primitive projections of unknown type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 2 insertions, 4 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 |