diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index e4cb1dede8..005b97a2b3 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2744,7 +2744,21 @@ primitives = Map.fromList
     , "`llvm_points_to`). The Term is the tuple consisting of the"
     , "output parameters of the LLVM function: the return parameter, then"
     , "the parameters passed by reference (in the order given by"
-    , "`llvm_points_to`). For more flexibility, see `llvm_verify`."
+    , "`llvm_points_to`)."
+    , ""
+    , "When invoking `llvm_compositional_extract mod fn_name term_name ovs"
+    , "check_path_sat spec strat`, the arguments represent the following:"
+    , "  1. `mod`: The LLVM module containing the function to extract."
+    , "  2. `fn_name`: The name of the function to extract."
+    , "  3. `term_name`: The name of the `Term` to generate."
+    , "  4. `ovs`: A list of overrides to use in the proof that the extracted"
+    , "     function satisifies `spec`."
+    , "  5. `check_path_sat`: Whether to perform path satisfiability checks."
+    , "  6. `spec`: SAW specification for the extracted function."
+    , "  7. `strat`: Proof strategy to use when verifying that the extracted"
+    , "     function satisfies `spec`."
+    , ""
+    , "For more flexibility, see `llvm_verify`."
     ]
   , prim "crucible_llvm_compositional_extract"
     "LLVMModule -> String -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"