diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5dbe95a471..aced97e910 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -398,8 +398,7 @@ struct match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.equal c1 c2 && Univ.Instance.equal u1 u2 - | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 | _, _ -> false in let rec equal_rec sk1 sk2 = @@ -1252,6 +1251,7 @@ let clos_whd_flags flgs env sigma t = let nf_beta = clos_norm_flags CClosure.beta let nf_betaiota = clos_norm_flags CClosure.betaiota let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta +let nf_zeta = clos_norm_flags CClosure.zeta let nf_all env sigma = clos_norm_flags CClosure.all env sigma |