diff options
| author | coqbot-app[bot] | 2020-11-20 08:51:20 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 08:51:20 +0000 |
| commit | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (patch) | |
| tree | 3b67df9afab90f5ae1d2aeddd3773a544dcbca95 /pretyping/evarconv.ml | |
| parent | f264aabf59866ae0d18509a7757e69c26e82f508 (diff) | |
| parent | 7265df1cda297603cb4eb74362df4463171c316a (diff) | |
Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 15 |
1 files changed, 6 insertions, 9 deletions
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 |