From 41e01ae58be6ebc617bab549b2699c30cef1abf9 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 6 Sep 2023 14:41:36 +0200 Subject: [PATCH] Update pretyping/evarconv.ml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Gaëtan Gilbert --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3a8341ee381e3..ff8b7fcfa9b67 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1154,7 +1154,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |Some _, Success _ -> UnifFailure (evd,NotSameHead) end - (* Catch the p.c ~= p c' cases *) + (* Catch the c.(p) ~= p c' cases *) | Proj (p1,c1), Const (p2,_) when QConstant.equal env (Projection.constant p1) p2 -> let c1 = try Some (destApp evd (Retyping.expand_projection env evd p1 c1 []))