Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 18 insertions, 24 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index b68123f6..667a0ed4 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -15,7 +15,7 @@ open Declarations
 open Sign
 (*i*)
 
-(*s Unsafe environments. We define here a datatype for environments. 
+(*s 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. *)
@@ -24,7 +24,7 @@ open Sign
    - a context for de Bruijn variables
    - a context for de Bruijn variables vm values
    - a context for section variables and goal assumptions
-   - a context for section variables and goal assumptions vm values 
+   - a context for section variables and goal assumptions vm values
    - a context for global constants and axioms
    - a context for inductive definitions
    - a set of universe constraints
@@ -55,7 +55,7 @@ val empty_context : env -> bool
 
 (************************************************************************)
 (*s Context of de Bruijn variables ([rel_context]) *)
-val nb_rel           : env -> int 
+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
@@ -80,12 +80,12 @@ val empty_named_context_val : named_context_val
 
 (* [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 : 
+   *** /!\ ***   [f t] should be convertible with t *)
+val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
 val push_named : named_declaration -> env -> env
-val push_named_context_val  : 
+val push_named_context_val  :
     named_declaration -> named_context_val -> named_context_val
 
 
@@ -98,7 +98,7 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
 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 *)
 
 val fold_named_context :
@@ -142,9 +142,6 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 (* raises [Not_found] if the required path is not found *)
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
-(* Find the ultimate inductive in the [mind_equiv] chain *)
-val scrape_mind : env -> mutual_inductive -> mutual_inductive
-
 (************************************************************************)
 (*s Modules *)
 val add_modtype : module_path -> module_type_body -> env -> env
@@ -155,10 +152,6 @@ 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
 
-val register_alias : module_path -> module_path -> env -> env
-val lookup_alias : module_path -> env -> module_path
-val scrape_alias : module_path -> env -> module_path
-
 (************************************************************************)
 (*s Universe constraints *)
 val set_universes   :   Univ.universes -> env -> env
@@ -168,10 +161,11 @@ val set_engagement : engagement -> env -> env
 
 (************************************************************************)
 (* Sets of referred section variables *)
-(* [global_vars_set env c] returns the list of [id]'s occurring as
-   [VAR id] in [c] *)
+(* [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 an atomic construction *)
+(* the constr must be a global reference *)
 val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
@@ -181,7 +175,7 @@ val keep_hyps : env -> Idset.t -> section_context
   actually only a datatype to store a term with its type and the type of its
   type. *)
 
-type unsafe_judgment = { 
+type unsafe_judgment = {
   uj_val  : constr;
   uj_type : types }
 
@@ -189,14 +183,14 @@ val make_judge : constr -> types -> unsafe_judgment
 val j_val  : unsafe_judgment -> constr
 val j_type : unsafe_judgment -> types
 
-type unsafe_type_judgment = { 
+type unsafe_type_judgment = {
   utj_val  : constr;
   utj_type : sorts }
 
 
 (*s Compilation of global declaration *)
 
-val compile_constant_body : 
+val compile_constant_body :
     env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
                                  (* opaque *) (* boxed *)
 
@@ -206,7 +200,7 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 
-val apply_to_hyp : named_context_val -> variable -> 
+val apply_to_hyp : named_context_val -> variable ->
   (named_context -> named_declaration -> named_context -> named_declaration) ->
     named_context_val
 
@@ -219,7 +213,7 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
       named_context_val
 
 val insert_after_hyp : named_context_val -> variable ->
-  named_declaration -> 
+  named_declaration ->
     (named_context -> unit) -> named_context_val
 
 val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
@@ -250,7 +244,7 @@ type context_object =
 module OrderedContextObject :  Set.OrderedType with type t = context_object
 module ContextObjectMap : Map.S with type key = context_object
 
-(* collects all the assumptions (optionally including opaque definitions) 
+(* collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type) *)
 val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t