mise en place programmation literaire (generation de doc/coq.tex)

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

1 files changed, 37 insertions, 27 deletions

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 058db0a11..46ffc42a1 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Generic
 open Term
@@ -8,33 +9,33 @@ open Univ
 open Environ
 open Closure
 open Evd
+(*i*)
+
+(* Reduction Functions. *)
 
 exception Redelimination
 exception Induc
 exception Elimconst
 
 type 'a reduction_function = 'a unsafe_env -> constr -> constr
-type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list 
-  -> constr * constr list
+
+type 'a stack_reduction_function = 
+    'a unsafe_env -> constr -> constr list -> constr * constr list
 
 val whd_stack : 'a stack_reduction_function
 
-(* Reduction Function Operators *)
-val under_casts      : 'a reduction_function -> 'a reduction_function
-val strong           : 'a reduction_function -> 'a reduction_function
+(*s Reduction Function Operators *)
+val under_casts : 'a reduction_function -> 'a reduction_function
+val strong : 'a reduction_function -> 'a reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
 
-(*************************
- ** Reduction Functions **
- *************************)
-
-(* Generic Optimized Reduction Functions using Closures *)
+(*s Generic Optimized Reduction Functions using Closures *)
 
 (* 1. lazy strategy *)
 val clos_norm_flags : Closure.flags -> 'a reduction_function
-(* Same as (strong whd_beta[delta][iota]), but much faster on big terms *) 
+(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
 val nf_beta : 'a reduction_function
 val nf_betaiota : 'a reduction_function
 val nf_betadeltaiota : 'a reduction_function
@@ -55,7 +56,7 @@ val whd_betaiota_stack : 'a stack_reduction_function
 val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
-(* Head normal forms *)
+(*s Head normal forms *)
 val whd_const_stack : section_path list -> 'a stack_reduction_function
 val whd_const : section_path list -> 'a reduction_function
 val whd_delta_stack : 'a stack_reduction_function
@@ -72,7 +73,7 @@ val whd_betadeltaiotaeta : 'a reduction_function
 val beta_applist : (constr * constr list) -> constr
 
 
-(* Special-Purpose Reduction Functions *)
+(*s Special-Purpose Reduction Functions *)
 val whd_meta : 'a reduction_function
 val plain_instance : 'a reduction_function
 val instance : 'a reduction_function
@@ -88,10 +89,14 @@ val one_step_reduce : 'a reduction_function
 val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
   'c unsafe_env -> string -> constr -> constr array -> constr
-val hnf_prod_applist : 'c unsafe_env -> string -> constr -> constr list -> constr
-val hnf_lam_app : 'c unsafe_env -> string -> constr -> constr -> constr
-val hnf_lam_appvect : 'c unsafe_env -> string -> constr -> constr array -> constr
-val hnf_lam_applist : 'c unsafe_env -> string -> constr -> constr list -> constr
+val hnf_prod_applist : 
+  'c unsafe_env -> string -> constr -> constr list -> constr
+val hnf_lam_app : 
+  'c unsafe_env -> string -> constr -> constr -> constr
+val hnf_lam_appvect : 
+  'c unsafe_env -> string -> constr -> constr array -> constr
+val hnf_lam_applist : 
+  'c unsafe_env -> string -> constr -> constr list -> constr
 val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr
 val decomp_prod : 'c unsafe_env -> constr -> int * constr
 val decomp_n_prod : 
@@ -110,7 +115,8 @@ val reduce_to_ind  : 'c unsafe_env -> constr ->
 
 val whd_programs : 'a reduction_function
 
-(* Generic reduction: reduction functions associated to tactics *)
+
+(*s Generic reduction: reduction functions associated to tactics *)
 type red_expr =
   | Red
   | Hnf
@@ -134,7 +140,7 @@ val compute : 'a reduction_function
 val reduction_of_redexp : red_expr -> 'a reduction_function
 
 
-(* Conversion Functions (uses closures, lazy strategy) *)
+(*s Conversion Functions (uses closures, lazy strategy) *)
 
 type conversion_result =
   | Convertible of universes
@@ -146,20 +152,24 @@ type 'a conversion_function =
 val sort_cmp : conv_pb -> sorts -> sorts -> universes -> conversion_result
 
 val fconv : conv_pb -> 'a conversion_function
+
 (* fconv has 4 instances:
- * conv   = fconv CONV   : conversion test, and adjust universes constraints
- * conv_x = fconv CONV_X :     id.        , without adjusting univ 
+   \begin{itemize}
+   \item [conv = fconv CONV] : 
+     conversion test, and adjust universes constraints
+   \item [conv_x = fconv CONV_X] : idem, without adjusting univ 
      (used in tactics)
- * conv_leq   = fconv CONV_LEQ   : cumulativity test, adjust universes
- * conv_x_leq = fconv CONV_X_LEQ :       id.        , without adjusting 
-     (in tactics)
- *)
+   \item [conv_leq = fconv CONV_LEQ] : cumulativity test, adjust universes
+   \item [conv_x_leq = fconv CONV_X_LEQ] : idem, without adjusting 
+     (used in tactics)
+   \end{itemize} *)
 val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 val conv_x : 'a conversion_function
 val conv_x_leq : 'a conversion_function
 
-(* Obsolete Reduction Functions *)
+
+(*s Obsolete Reduction Functions *)
 
 val hnf : 'a unsafe_env -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
@@ -171,5 +181,5 @@ val check_mrectype_spec : 'a unsafe_env -> constr -> constr
 val minductype_spec : 'a unsafe_env -> constr -> constr
 val mrectype_spec : 'a unsafe_env -> constr -> constr
 
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
+(* Special function, which keep the key casts under Fix and MutCase. *)
 val strip_all_casts : constr -> constr