Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

1 files changed, 14 insertions, 4 deletions

diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 52cdabc06b..0969387fb1 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -9,20 +9,30 @@ open Environ
 open Evarutil
 (*i*)
 
-(* Coercions. *)
+(*s Coercions. *)
 
 val inh_app_fun :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_tosort_force :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+
+(* [inh_tosort env sigma j] insert a coercion into [j], if needed, in
+   such a way [t] reduces to a sort; it fails if no coercion is applicable *)
 val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_ass_of_j : 
+
+val inh_ass_of_j :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
 
+(* [inh_conv_coerce_to loc env sigma j t] insert a coercion into [j],
+   if needed, in such a way it [t] and [j.uj_type] are convertible; it
+   fails if no coercion is applicable *)
 val inh_conv_coerce_to : Rawterm.loc ->
-  env -> 'a evar_defs -> unsafe_judgment -> typed_type -> unsafe_judgment
+  env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
 
-val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs ->
+(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
+   args)] of type [tycon] (if any) by inserting coercions in front of
+   each arg$_i$, if necessary *)
+val inh_apply_rel_list : Rawterm.loc -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> constr option
     -> unsafe_judgment