Allow Print DependGraph to accept a list of references

Changed the command syntax from accepting a single reference to accepting
a reference_list, enabling users to generate dependency graphs for multiple
definitions in a single command.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: 2 people

README.md

@@ -141,11 +141,11 @@ The available commands are :
     Take all the objects of the specified modules and build the dependencies
     between them.
 
-- Generate the dependencies of one objects:
+- Generate the dependencies of one or more objects:
 
-        Print DependGraph my_lemma.
+        Print DependGraph my_lemma my_other_lemma.
 
-  Analyse recursively the dependencies of ``my_lemma``.
+  Analyse recursively the dependencies of the given objects.
 
 - Change the name of the generated file (default is ``graph.dpd``):
 

graphdepend.mlg

@@ -243,10 +243,10 @@ end = struct
       error (str "cannot open file: " ++ (str msg));
 end
 
-let mk_dpds_graph opaque_access gref =
+let mk_dpds_graph opaque_access grefs =
   let graph = G.empty in
   let all = true in (* get all the dependencies recursively *)
-  let graph = add_gref_list_and_dpds opaque_access graph ~all [gref] in
+  let graph = add_gref_list_and_dpds opaque_access graph ~all grefs in
     Out.file graph
 
 let file_graph_depend opaque_access dirlist =
@@ -280,8 +280,8 @@ END
 *)
 
 VERNAC COMMAND EXTEND DependGraph CLASSIFIED AS QUERY STATE opaque_access
-  | ["Print" "DependGraph" reference(ref) ] ->
-      { fun ~opaque_access -> mk_dpds_graph opaque_access (Nametab.global ref) }
+  | ["Print" "DependGraph" reference_list(refs) ] ->
+      { fun ~opaque_access -> mk_dpds_graph opaque_access (List.map Nametab.global refs) }
   | ["Print" "FileDependGraph" reference_list(dl) ] ->
       { fun ~opaque_access ->
         file_graph_depend opaque_access (List.map locate_mp_dirpath dl) }

meta.yml

@@ -168,11 +168,11 @@ documentation: |
       Take all the objects of the specified modules and build the dependencies
       between them.
   
-  - Generate the dependencies of one objects:
-  
-          Print DependGraph my_lemma.
-  
-    Analyse recursively the dependencies of ``my_lemma``.
+  - Generate the dependencies of one or more objects:
+
+          Print DependGraph my_lemma my_other_lemma.
+
+    Analyse recursively the dependencies of the given objects.
   
   - Change the name of the generated file (default is ``graph.dpd``):