Extend `Print Canonical Projections` with a search functionality

The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.

6 files changed, 25 insertions, 8 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 436648c163..69ab0fafe9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram
       | IDENT "Coercions" -> { PrintCoercions }
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> { PrintCoercionPaths (s,t) }
-      | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+      | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global
+         -> { PrintCanonicalConversions qids }
       | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
       | IDENT "Tables" -> { PrintTables }
       | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1742027076..a1bd99c237 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function
       keyword "Print Coercion Paths" ++ spc()
       ++ pr_class_rawexpr s ++ spc()
       ++ pr_class_rawexpr t
-    | PrintCanonicalConversions ->
-      keyword "Print Canonical Structures"
+    | PrintCanonicalConversions qids ->
+      keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
     | PrintTypingFlags ->
       keyword "Print Typing Flags"
     | PrintTables ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index d04a02febc..8ced35c3be 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -996,12 +996,26 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
-let print_canonical_projections env sigma =
+let print_canonical_projections env sigma grefs =
+  let match_proj_gref ((x,y),c) gr =
+    GlobRef.equal x gr ||
+    begin match y with
+      | Const_cs y -> GlobRef.equal y gr
+      | _ -> false
+    end ||
+    match gr with
+    | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con
+    | _ -> false
+  in
+  let projs =
+    List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
+      (canonical_projections ())
+  in
   prlist_with_sep fnl
     (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
     str " <- " ++
     pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
-    (canonical_projections ())
+    projs
 
 (*************************************************************************)
 
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index 2ee9c4ed33..ac41f30c5d 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -53,7 +53,7 @@ val print_graph : unit -> Pp.t
 val print_classes : unit -> Pp.t
 val print_coercions : unit -> Pp.t
 val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
-val print_canonical_projections : env -> Evd.evar_map -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> GlobRef.t list -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 604d1b28ff..04f3e0d7b2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1701,7 +1701,9 @@ let vernac_print ~pstate ~atts =
   | PrintCoercions -> Prettyp.print_coercions ()
   | PrintCoercionPaths (cls,clt) ->
     Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
-  | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
+  | PrintCanonicalConversions qids ->
+    let grefs = List.map Smartlocate.smart_global qids in
+    Prettyp.print_canonical_projections env sigma grefs
   | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
   | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
   | PrintHintGoal ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 32ff8b8fb2..1daa244986 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -46,7 +46,7 @@ type printable =
   | PrintInstances of qualid or_by_notation
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
-  | PrintCanonicalConversions
+  | PrintCanonicalConversions of qualid or_by_notation list
   | PrintUniverses of bool * qualid list option * string option
   | PrintHint of qualid or_by_notation
   | PrintHintGoal