Update pretyping/evarconv.ml

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
coq · Sep 6, 2023 · 41e01ae · 41e01ae
1 parent b944827
commit 41e01ae
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 []))