Coq: Missing typing colon in the output of the Search ssreflect vernacular

[erikmd]

Description of the problem

Previously reported in math-comp/math-comp#50

This issue had been fixed in math-comp/math-comp#73 but not in the SSR plugin shipped in Coq.

To reproduce the issue:

From Coq Require Import ssreflect.
Search _ "ssr".

Expected result

ssr_converse: forall R : Type, R -> True * R
ssr_have: forall Plemma Pgoal : Type, Plemma -> (Plemma -> Pgoal) -> Pgoal
ssr_have_let: forall (Pgoal Plemma : Type) (step : Plemma), (let x := step in Pgoal) -> Pgoal
ssr_suff: forall Plemma Pgoal : Type, (Plemma -> Pgoal) -> Plemma -> Pgoal
ssr_wlog: forall Plemma Pgoal : Type, (Plemma -> Pgoal) -> Plemma -> Pgoal
ssr_congr_arrow: forall Plemma Pgoal : Type, Plemma = Pgoal -> Plemma -> Pgoal

Actual result

ssr_converse  forall R : Type, R -> True * R
ssr_have  forall Plemma Pgoal : Type, Plemma -> (Plemma -> Pgoal) -> Pgoal
ssr_have_let  forall (Pgoal Plemma : Type) (step : Plemma), (let x := step in Pgoal) -> Pgoal
ssr_suff  forall Plemma Pgoal : Type, (Plemma -> Pgoal) -> Plemma -> Pgoal
ssr_wlog  forall Plemma Pgoal : Type, (Plemma -> Pgoal) -> Plemma -> Pgoal
ssr_congr_arrow  forall Plemma Pgoal : Type, Plemma = Pgoal -> Plemma -> Pgoal

Coq Version

47f202605b4ef1795a31312b3ff2eda006fa46a6

[Zimmi48]

Congrats on submitting #10000 :tada: