retablissement make doc et make minicoq

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

5 files changed, 18 insertions, 16 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 616a11162..981be607f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -49,21 +49,21 @@ val names_of_rel_context : env -> names_context
 (*s Returns also the substitution to be applied to rel's *)
 val push_rels_to_vars : env -> constr list * env
 
-(* Gives identifiers in var_context and rel_context *)
+(* Gives identifiers in [var_context] and [rel_context] *)
 val ids_of_context : env -> identifier list
 val map_context : (constr -> constr) -> env -> env
 
-(*s Recurrence on var_context *)
+(*s Recurrence on [var_context] *)
 val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
 val process_var_context : (env -> var_declaration -> env) -> env -> env
 
 (* [process_var_context_both_sides f env] iters [f] on the var
-   declarations of env taking as argument both the initial segment, the
+   declarations of [env] taking as argument both the initial segment, the
    middle value and the tail segment *)
 val process_var_context_both_sides :
   (env -> var_declaration -> var_context -> env) -> env -> env 
 
-(*s Recurrence on rel_context *)
+(*s Recurrence on [rel_context] *)
 val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
 val process_rel_context : (env -> rel_declaration -> env) -> env -> env
 
@@ -81,13 +81,13 @@ val new_meta : unit -> int
 
 (*s Looks up in environment *)
 
-(* Looks up in the context of local vars referred by names (var_context) *)
+(* Looks up in the context of local vars referred by names ([var_context]) *)
 (* raises [Not_found] if the identifier is not found *)
 val lookup_var_type : identifier -> env -> typed_type
 val lookup_var_value : identifier -> env -> constr option
 val lookup_var : identifier -> env -> constr option * typed_type
 
-(* Looks up in the context of local vars referred by indice (rel_context) *)
+(* Looks up in the context of local vars referred by indice ([rel_context]) *)
 (* raises [Not_found] if the index points out of the context *)
 val lookup_rel_type : int -> env -> name * typed_type
 val lookup_rel_value : int -> env -> constr option
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6d8c80bd0..c2fb4a3c0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -28,10 +28,10 @@ val var_context : safe_environment -> var_context
 
 val push_var_decl : identifier * constr -> safe_environment -> safe_environment
 val push_var_def : identifier * constr -> safe_environment -> safe_environment
-(*
+(*i
 val push_rel_decl : name * constr -> safe_environment -> safe_environment
 val push_rel_def : name * constr -> safe_environment -> safe_environment
-*)
+i*)
 
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
@@ -48,9 +48,9 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 val pop_vars : identifier list -> safe_environment -> safe_environment
 
 val lookup_var : identifier -> safe_environment -> constr option * typed_type
-(*
+(*i
 val lookup_rel : int -> safe_environment -> name * typed_type
-*)
+i*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
 val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 3add55894..17d9267d9 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,13 +7,15 @@ open Generic
 open Term
 (*i*)
 
-(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+(*s Signatures of ordered named variables, intended to be accessed by name *)
 
 type var_context = var_declaration list
 
-val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var : 
+  identifier * constr option * typed_type -> var_context -> var_context
 val add_var_decl : identifier * typed_type -> var_context -> var_context
-val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val add_var_def : 
+  identifier * constr * typed_type -> var_context -> var_context
 val lookup_id : identifier -> var_context -> constr option * typed_type
 val lookup_id_type : identifier -> var_context -> typed_type
 val lookup_id_value : identifier -> var_context -> constr option 
diff --git a/kernel/term.mli b/kernel/term.mli
index 9019fa091..cd86af675 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -100,7 +100,7 @@ type 'ctxt reference =
 
 (* Concrete type for making pattern-matching. *)
 
-(* [constr array] is an instance matching definitional var_context in
+(* [constr array] is an instance matching definitional [var_context] in
    the same order (i.e. last argument first) *)
 type existential = int * constr array
 type constant = section_path * constr array
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a07206fb0..a2fedf7f1 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -84,7 +84,7 @@ open Inductive
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
-(*
+(*i
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
-*)
+i*)