Mod_subst: some simplifications, some more significant names to functions, etc

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

1 files changed, 32 insertions, 29 deletions

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 90b3d8c69..55d2ff15a 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -11,64 +11,55 @@
 open Names
 open Term
 
-(** A delta_resolver maps name (constant, inductive, module_path) 
+(** {6 Delta resolver} *)
+
+(** A delta_resolver maps name (constant, inductive, module_path)
    to canonical name  *)
 type delta_resolver
 
-type substitution
-
 val empty_delta_resolver : delta_resolver
 
-val add_inline_delta_resolver :
-  constant -> int -> delta_resolver -> delta_resolver
-
-val add_inline_constr_delta_resolver :
-  constant -> int -> constr -> delta_resolver -> delta_resolver
-
-val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
+val add_mp_delta_resolver :
+  module_path -> module_path -> delta_resolver -> delta_resolver
 
-val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver
+val add_kn_delta_resolver :
+  kernel_name -> kernel_name -> delta_resolver -> delta_resolver
 
-val add_mp_delta_resolver : module_path -> module_path -> delta_resolver 
-  -> delta_resolver
+val add_inline_delta_resolver :
+  kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
-(** Apply the substitution on the domain of the resolver  *)
-val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
-
-(** Apply the substitution on the codomain of the resolver  *)
-val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+(** Effect of a [delta_resolver] on kernel name, constant, inductive, etc *)
 
-val subst_dom_codom_delta_resolver : 
-  substitution -> delta_resolver -> delta_resolver
-
-(** *_of_delta return the associated name of arg2 in arg1   *)
+val kn_of_delta : delta_resolver -> kernel_name -> kernel_name
 val constant_of_delta_kn : delta_resolver -> kernel_name -> constant
 val constant_of_delta : delta_resolver -> constant -> constant
 
 val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive
 val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
-val delta_of_mp : delta_resolver -> module_path -> module_path
+val mp_of_delta : delta_resolver -> module_path -> module_path
 
 (** Extract the set of inlined constant in the resolver *)
 val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
 
-(** mem tests *)
-val mp_in_delta : module_path -> delta_resolver -> bool
+(** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *)
 
+val mp_in_delta : module_path -> delta_resolver -> bool
 val con_in_delta : constant -> delta_resolver -> bool
-
 val mind_in_delta : mutual_inductive -> delta_resolver -> bool
 
-(*substitution*)
+
+(** {6 Substitution} *)
+
+type substitution
 
 val empty_subst : substitution
 
 val is_empty_subst : substitution -> bool
 
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no 
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
    sequential composition  *)
 val add_mbid :
   mod_bound_id -> module_path -> delta_resolver  -> substitution -> substitution
@@ -86,6 +77,18 @@ val map_mp :
 *)
 val join : substitution -> substitution -> substitution
 
+
+(** Apply the substitution on the domain of the resolver  *)
+val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+
+(** Apply the substitution on the codomain of the resolver  *)
+val subst_codom_delta_resolver :
+  substitution -> delta_resolver -> delta_resolver
+
+val subst_dom_codom_delta_resolver :
+  substitution -> delta_resolver -> delta_resolver
+
+
 type 'a substituted
 val from_val : 'a -> 'a substituted
 val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
@@ -109,7 +112,7 @@ val subst_mp :
 val subst_ind :
   substitution -> mutual_inductive -> mutual_inductive
 
-val subst_kn : 
+val subst_kn :
   substitution -> kernel_name -> kernel_name
 
 val subst_con :