diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index b160594f14..fe8a888a6d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -567,10 +567,10 @@ type constr_operator = val splay_constr : constr -> constr_operator * constr array val gather_constr : constr_operator * constr array -> constr -(* +(*i val splay_constr : ('a,'a)kind_of_term -> constr_operator * 'a array val gather_constr : constr_operator * 'a array -> ('a,'a) kind_of_term -*) +i*) val splay_constr_with_binders : constr -> constr_operator * rel_declaration list * constr array val gather_constr_with_binders : |