diverses modifs pour ocamlweb

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

2 files changed, 28 insertions, 24 deletions

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