From 44e7cd6dd3d4f50391c20bd27176fff30e1da33c Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 14 Sep 2000 13:22:58 +0000
Subject: Minor correction for Ocamlweb + doc update

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@608 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index efec41d42e..ede13abea0 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,14 +15,19 @@ exception Redelimination
 
 (* Red (raise Redelimination if nothing reducible) *)
 val red_product : 'a reduction_function
+
 (* Hnf *)
 val hnf_constr : 'a reduction_function
+
 (* Simpl *)
 val nf : 'a reduction_function
+
 (* Unfold *)
 val unfoldn : (int list * section_path) list -> 'a reduction_function
+
 (* Fold *)
 val fold_commands : constr list -> 'a reduction_function
+
 (* Pattern *)
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 (* Rem: Lazy strategies are defined in Reduction *)
@@ -32,7 +37,7 @@ val cbv_norm_flags : Closure.flags -> 'a reduction_function
   val cbv_beta : 'a reduction_function
   val cbv_betaiota : 'a reduction_function
   val cbv_betadeltaiota : 'a reduction_function
-  val compute : 'a reduction_function  (* = cbv_betadeltaiota *)
+  val compute : 'a reduction_function  (* = [cbv_betadeltaiota] *)
 
 val one_step_reduce : 'a reduction_function
 
-- 
cgit v1.2.3