From f7967b6c3e03dabe71cf38d51557b4d94253ae75 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 12 Dec 2000 15:58:10 +0000
Subject: Hint Unfold Local + commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1088 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0c9ec04844..2768bb3fea 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -542,7 +542,7 @@ let unfold env sigma name =
   clos_norm_flags (unfold_flags name) env sigma
 
 
-(* unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)
+(* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
-- 
cgit v1.2.3