improve doc

LPCIC · Oct 21, 2023 · f2038ac · f2038ac
1 parent 995505a
commit f2038ac
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -1666,8 +1666,10 @@ external pred coq.term->string i:term, o:string.
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 
-% [coq.extra-dep Identifier File Name] Resolve the file name of an Extra
-% Dependency
+% -- Extra Dependencies -----------------------------------------------
+
+% [coq.extra-dep Identifier FileName] Resolve the file name of an extra
+% dependency. See also Coq's From xxx Extra Dependency yyy as zzz.
 external pred coq.extra-dep i:id, o:option id.
 
 % -- Access to Elpi's data --------------------------------------------

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -3888,8 +3888,8 @@ Supported attributes:
 
   MLCode(Pred("coq.extra-dep",
     In(id, "Identifier",
-    Out(option id, "File Name",
-    Easy "Resolve the file name of an Extra Dependency")),
+    Out(option id, "FileName",
+    Easy "Resolve the file name of an extra dependency. See also Coq's From xxx Extra Dependency yyy as zzz.")),
   (fun id _ ~depth ->
     !: (try Some (ComExtraDeps.query_extra_dep (Names.Id.of_string id))
         with Not_found -> None))),