aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.ml
diff options
context:
space:
mode:
authorfilliatr2000-05-03 20:44:42 +0000
committerfilliatr2000-05-03 20:44:42 +0000
commitbae7532aaf4fc4ca0f637cb6e53f6b4b80c7cb75 (patch)
treee4c5a1725f1d12b78b959e974f61380f55557806 /kernel/term.ml
parent5c64bc0eb899409b66b3e13fe99ebf679b0850a7 (diff)
diverses modifs pour ocamlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 16d63fcbfc..111bcfbf3c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1649,4 +1649,4 @@ let constr_display csr=
Name(id) -> "Name("^(string_of_id id)^")"
|Anonymous -> "Anonymous"
in
- mSG [<'sTR (term_display csr);'fNL>];;
+ mSG [<'sTR (term_display csr);'fNL>]