diverses modifs pour ocamlweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 42 insertions, 34 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>]
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*)
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index 289706fdb9..de3a022862 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,8 +1,10 @@
 
+(*i*)
 open Pp
 open Names
 open Term
 open Sign
+(*i*)
 
 val term : constr Grammar.Entry.e
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 9bd4827636..f46f9ddb3d 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -12,7 +12,7 @@ open Evarutil
 (*i*)
 
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
-   on unresolved evars, or replace them by Metas ; the unsafe_judgment list
+   on unresolved evars, or replace them by Metas ; the [unsafe_judgment] list
    allows us to extend env with some bindings *)
 val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
   env -> (identifier * unsafe_judgment) list ->
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index eaebd6b992..9c2ac00ae4 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -1,3 +1,6 @@
+
+(* $Id$ *)
+
 (*i*)
 open Environ
 open Evd
@@ -7,8 +10,8 @@ open Term
 open Util
 (*i*)
 
-(*This module defines the structure of proof tree and the tactic type. So, it
-  is used by Proof_tree and Refiner*)
+(* This module defines the structure of proof tree and the tactic type. So, it
+   is used by [Proof_tree] and [Refiner] *)
 
 type bindOcc = 
   | Dep of identifier
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 87d5e2a1ff..9f82d30e7b 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -9,37 +9,38 @@ open Tacmach
 open Term
 (*i*)
 
-(*Values for interpretation*)
-type value=
-   VTactic of tactic
-  |VFTactic of tactic_arg list*(tactic_arg list->tactic)
-  |VRTactic of (goal list sigma * validation)
-  |VArg of tactic_arg
-  |VFun of (string*value) list*string option list*Coqast.t
-  |VVoid
-  |VRec of value ref;;
+(* Values for interpretation *)
+type value =
+  | VTactic of tactic
+  | VFTactic of tactic_arg list * (tactic_arg list -> tactic)
+  | VRTactic of (goal list sigma * validation)
+  | VArg of tactic_arg
+  | VFun of (string * value) list * string option list * Coqast.t
+  | VVoid
+  | VRec of value ref
 
-(*Gives the constr corresponding to a CONSTR tactic_arg*)
-val constr_of_Constr:tactic_arg-> constr;;
+(* Gives the constr corresponding to a CONSTR [tactic_arg] *)
+val constr_of_Constr : tactic_arg -> constr
 
-(*Signature for interpretation: val_interp and interpretation functions*)
-type interp_sign=
-  evar_declarations*Environ.env*(string*value) list*(int*constr) list*
-    goal sigma option;;
+(* Signature for interpretation: [val_interp] and interpretation functions *)
+type interp_sign =
+  evar_declarations * Environ.env * (string * value) list * 
+    (int * constr) list * goal sigma option
 
-(*Adds a Tactic Definition in the table*)
-val add_tacdef : string -> value -> unit;;
+(* Adds a Tactic Definition in the table *)
+val add_tacdef : string -> value -> unit
 
-(*Interprets any expression*)
-val val_interp:interp_sign->Coqast.t->value;;
+(*Interprets any expression *)
+val val_interp : interp_sign -> Coqast.t -> value
+
+(* Interprets tactic arguments *)
+val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
 
-(*Interprets tactic arguments*)
-val interp_tacarg:interp_sign->Coqast.t->tactic_arg;;
 
 val interp               : Coqast.t -> tactic
 val vernac_interp        : Coqast.t -> tactic
 val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
 
-val is_just_undef_macro     : Coqast.t -> string option
+val is_just_undef_macro  : Coqast.t -> string option
 
 val bad_tactic_args : string -> 'a
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3ec63908fe..0161343071 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -63,7 +63,8 @@ val get_pat            : marked_pattern -> constr_pattern
 
 type marked_term
 val put_squel          : module_mark -> string -> marked_term
-(*val get_squel          : marked_term -> constr*)
+
+(*i val get_squel          : marked_term -> constr i*)
 
 (*i Remplacé par Astterm.interp_constrpattern
 val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
@@ -98,7 +99,7 @@ val get_reference : string list -> string -> constr
 (* [dest_somatch c pat] matches [c] against [pat] and returns the resulting
    assignment of metavariables; it raises [PatternMatchingFailure] if
    not matchable *)
-(*
+(*i
 val dest_somatch : constr -> marked_pattern -> constr list
 
 (* [somatches c pat] just tells if [c] matches against [pat] *)
@@ -117,7 +118,7 @@ val dest_somatch_conv :
 
 val somatches_conv :
   Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
-*)
+i*)
 
 val soinstance   : marked_term -> constr list -> constr 
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ae38c210e4..de91973d62 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -48,10 +48,10 @@ val tclTHEN_i1     : tactic -> (int -> tactic) -> tactic
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
-(*
+(*i
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
-*)
+i*)
 val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool