diff options
| author | filliatr | 2001-04-02 14:57:08 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-02 14:57:08 +0000 |
| commit | 6c3d91323125c08ecce3d0e03952706361f380b0 (patch) | |
| tree | fea7f4fc200f16b9b5c2f747684efef2234e1e9f /kernel | |
| parent | 45b2102f6bfd5b5739a5b5c8d4bb47587810429f (diff) | |
mise a jour pour ocamlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1517 85f007b7-540e-0410-9357-904b9bb8a0f7
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 : |