diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 6 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 5 |
2 files changed, 3 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, [] |