From bae7532aaf4fc4ca0f637cb6e53f6b4b80c7cb75 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 3 May 2000 20:44:42 +0000
Subject: diverses modifs pour ocamlweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml     | 2 +-
 kernel/term.mli    | 6 +++---
 kernel/typeops.mli | 1 +
 3 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel')

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>]
diff --git a/kernel/term.mli b/kernel/term.mli
index 145546b55c..69db204fb0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -515,8 +515,8 @@ val sort_hdchar : sorts -> string
 
 val occur_meta : constr -> bool
 
-(*Returns the maximum of metas. Returns -1 if there is no meta*)
-(*val max_occur_meta:constr->int;;*)
+(*i Returns the maximum of metas. Returns -1 if there is no meta i*)
+(*i val max_occur_meta : constr -> int i*)
 
 val occur_existential : constr -> bool
 val rel_vect : int -> int -> constr array
@@ -562,4 +562,4 @@ val hcons_constr:
 
 val hcons1_constr : constr -> constr
 
-val constr_display: constr -> unit;;
+val constr_display: constr -> unit
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 5411354420..2c93141cbe 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,3 +1,4 @@
+
 (* $Id$ *)
 
 (*i*)
-- 
cgit v1.2.3