aboutsummaryrefslogtreecommitdiff
path: root/kernel/sosub.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/sosub.mli')
-rw-r--r--kernel/sosub.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/sosub.mli b/kernel/sosub.mli
index c3093af730..531b7ee7e1 100644
--- a/kernel/sosub.mli
+++ b/kernel/sosub.mli
@@ -1,7 +1,11 @@
(* $Id$ *)
+(*i*)
open Term
+(*i*)
+
+(* Second-order substitutions. *)
val soexecute : constr -> constr
val try_soexecute : constr -> constr