diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 12 |
2 files changed, 10 insertions, 4 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 38b26d06b9..a7ebd5f9f5 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with let same_proj sigma t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with - | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2 | _ -> false let all_ok _ _ = true diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4a907b2795..91cd5b251c 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -309,9 +309,15 @@ END ~category:"deprecated" ~default:CWarnings.Enabled (fun () -> (Pp.strbrk - "SSReflect's Search command has been moved to the \ - ssrsearch module; please Require that module if you \ - still want to use SSReflect's Search command")) + "In previous versions of Coq, loading SSReflect had the effect of \ + replacing the built-in 'Search' command with an SSReflect version \ + of that command. \ + Coq's own search feature was still available via 'SearchAbout' \ + (but that alias is deprecated). \ + This replacement no longer happens; now 'Search' calls Coq's own search \ + feature even when SSReflect is loaded. \ + If you want to use SSReflect's deprecated Search command \ + instead of the built-in one, please Require the ssrsearch module.")) open G_vernac } |