From 677cf7db31c0dbf2f138ba2d25063737dfc662c5 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 09:07:25 +0000
Subject: documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacticals.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 49acb49e44..4ac1fb41d0 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -73,9 +73,9 @@ val ifOnClause     :
   (clause * constr -> bool) -> (clause -> tactic) -> (clause -> tactic) -> 
     clause -> tactic
 
-(*i Usage : [ConclPattern concl pat tacast]
+(* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
-   Pattern.somatches, then replace ?1 ?2 metavars in tacast by the
+   [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
 val conclPattern : constr -> constr -> Coqast.t -> tactic
-- 
cgit v1.2.3