Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 51 insertions, 54 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index a7795136..42100e4e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,26 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Term
 open Declarations
 open Sign
-(*i*)
 
-(*s Unsafe environments. We define here a datatype for environments.
+(** Unsafe environments. We define here a datatype for environments.
    Since typing is not yet defined, it is not possible to check the
    informations added in environments, and that is why we speak here
    of ``unsafe'' environments. *)
 
-(* Environments have the following components:
+(** Environments have the following components:
    - a context for de Bruijn variables
    - a context for de Bruijn variables vm values
    - a context for section variables and goal assumptions
@@ -50,27 +46,27 @@ val named_context_val : env -> named_context_val
 
 val engagement    : env -> engagement option
 
-(* is the local context empty *)
+(** is the local context empty *)
 val empty_context : env -> bool
 
-(************************************************************************)
-(*s Context of de Bruijn variables ([rel_context]) *)
+(** {5 Context of de Bruijn variables ([rel_context]) } *)
+
 val nb_rel           : env -> int
 val push_rel         : rel_declaration -> env -> env
 val push_rel_context :     rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
-(* Looks up in the context of local vars referred by indice ([rel_context]) *)
-(* raises [Not_found] if the index points out of the 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    : int -> env -> rel_declaration
 val evaluable_rel : int -> env -> bool
 
-(*s Recurrence on [rel_context] *)
+(** {6 Recurrence on [rel_context] } *)
+
 val fold_rel_context :
   (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-(************************************************************************)
-(* Context of variables (section variables and goal assumptions) *)
+(** {5 Context of variables (section variables and goal assumptions) } *)
 
 val named_context_of_val : named_context_val -> named_context
 val named_vals_of_val : named_context_val -> Pre_env.named_vals
@@ -78,7 +74,7 @@ val val_of_named_context : named_context -> named_context_val
 val empty_named_context_val : named_context_val
 
 
-(* [map_named_val f ctxt] apply [f] to the body and the type of
+(** [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
 val map_named_val :
@@ -90,8 +86,8 @@ val push_named_context_val  :
 
 
 
-(* Looks up in the context of local vars referred by names ([named_context]) *)
-(* raises [Not_found] if the identifier is not found *)
+(** Looks up in the context of local vars referred by names ([named_context]) 
+   raises [Not_found] if the identifier is not found *)
 
 val lookup_named     : variable -> env -> named_declaration
 val lookup_named_val : variable -> named_context_val -> named_declaration
@@ -99,34 +95,36 @@ val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
 
-(*s Recurrence on [named_context]: older declarations processed first *)
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
 
 val fold_named_context :
   (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-(* Recurrence on [named_context] starting from younger decl *)
+(** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
 
-(* This forgets named and rel contexts *)
+(** This forgets named and rel contexts *)
 val reset_context : env -> env
-(* This forgets rel context and sets a new named context *)
+
+(** This forgets rel context and sets a new named context *)
 val reset_with_named_context : named_context_val -> env -> env
 
-(************************************************************************)
-(*s Global constants *)
-(*s Add entries to global environment *)
-val add_constant : constant -> constant_body -> env -> env
+(** {5 Global constants }
+  {6 Add entries to global environment } *)
 
-(* Looks up in the context of global constant names *)
-(* raises [Not_found] if the required path is not found *)
+val add_constant : constant -> constant_body -> env -> env
 
+(** Looks up in the context of global constant names 
+   raises [Not_found] if the required path is not found *)
 val lookup_constant    : constant -> env -> constant_body
 val evaluable_constant : constant -> env -> bool
 
-(*s [constant_value env c] raises [NotEvaluableConst Opaque] if
+(** {6 ... } *)
+(** [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
    body and [Not_found] if it does not exist in [env] *)
+
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
@@ -134,44 +132,44 @@ val constant_value     : env -> constant -> constr
 val constant_type      : env -> constant -> constant_type
 val constant_opt_value : env -> constant -> constr option
 
-(************************************************************************)
-(*s Inductive types *)
+(** {5 Inductive types } *)
+
 val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 
-(* Looks up in the context of global inductive names *)
-(* raises [Not_found] if the required path is not found *)
+(** Looks up in the context of global inductive names 
+   raises [Not_found] if the required path is not found *)
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
-(************************************************************************)
-(*s Modules *)
+(** {5 Modules } *)
+
 val add_modtype : module_path -> module_type_body -> env -> env
 
-(* [shallow_add_module] does not add module components *)
+(** [shallow_add_module] does not add module components *)
 val shallow_add_module : module_path -> module_body -> env -> env
 
 val lookup_module : module_path -> env -> module_body
 val lookup_modtype : module_path -> env -> module_type_body
 
-(************************************************************************)
-(*s Universe constraints *)
-val set_universes   :   Univ.universes -> env -> env
+(** {5 Universe constraints } *)
+
 val add_constraints : Univ.constraints -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-(************************************************************************)
-(* Sets of referred section variables *)
-(* [global_vars_set env c] returns the list of [id]'s occurring either
+(** {6 Sets of referred section variables }
+   [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
    dependent in a global reference occurring in [c] *)
+
 val global_vars_set : env -> constr -> Idset.t
-(* the constr must be a global reference *)
+
+(** the constr must be a global reference *)
 val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
 
-(************************************************************************)
-(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
+(** {5 Unsafe judgments. }
+    We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
   type. *)
 
@@ -188,23 +186,20 @@ type unsafe_type_judgment = {
   utj_type : sorts }
 
 
-(*s Compilation of global declaration *)
+(** {6 Compilation of global declaration } *)
 
-val compile_constant_body :
-    env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
-                                 (* opaque *) (* boxed *)
+val compile_constant_body : env -> constant_def -> Cemitcodes.body_code
 
 exception Hyp_not_found
 
-(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
+(** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
-
 val apply_to_hyp : named_context_val -> variable ->
   (named_context -> named_declaration -> named_context -> named_declaration) ->
     named_context_val
 
-(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
+(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
    [tail::(id,_,_)::head] and
    return [(g tail)::(f (id,_,_))::head]. *)
 val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
@@ -219,9 +214,10 @@ val insert_after_hyp : named_context_val -> variable ->
 val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
 
 
-(* spiwack: functions manipulating the retroknowledge *)
-open Retroknowledge
 
+open Retroknowledge
+(** functions manipulating the retroknowledge 
+    @author spiwack *)
 val retroknowledge : (retroknowledge->'a) -> env -> 'a
 
 val registered : env -> field -> bool
@@ -230,3 +226,4 @@ val unregister : env -> field -> env
 
 val register : env -> field -> Retroknowledge.entry -> env
 
+