From 78d1c75322684eaa7e0ef753ee56d9c6140ec830 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 13 Dec 2001 09:03:13 +0000 Subject: compat ocaml 3.03 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/dhyp.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'tactics/dhyp.ml') diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 839c63978..10e4230d6 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -77,7 +77,7 @@ hypothesis" is defined in this way: Require DHyp. Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1 - [<:tactic:>]. + (:tactic:). Then, the tactic is used like this: @@ -91,7 +91,7 @@ hypothesis H. Similarly for the conclusion : -Hint Destruct Conclusion equal_zero (? = ?) 1 [<:tactic:>]. +Hint Destruct Conclusion equal_zero (? = ?) 1 (:tactic:). Goal (plus O O)=O. DConcl. @@ -101,7 +101,7 @@ The "Discardable" option clears the hypothesis after using it. Require DHyp. Hint Destruct Discardable Hypothesis less_than_zero (le (S ?) O) 1 - [<:tactic:>]. + (:tactic:). Goal (n:nat)(le (S n) O) -> False. Intros n H. @@ -174,8 +174,8 @@ let add (na,dd) = | Concl p -> p.d_typ in if Nbtermdn.in_dn tactab na then begin - mSGNL [< 'sTR "Warning [Overriding Destructor Entry " ; - 'sTR (string_of_id na) ; 'sTR"]" >]; + msgnl (str "Warning [Overriding Destructor Entry " ++ + str (string_of_id na) ++ str"]"); Nbtermdn.remap tactab na (pat,dd) end else Nbtermdn.add tactab (na,(pat,dd)) @@ -192,8 +192,8 @@ let cache_dd (_,(na,dd)) = add (na,dd) with _ -> anomalylabstrm "Dhyp.add" - [< 'sTR"The code which adds destructor hints broke;"; 'sPC; - 'sTR"this is not supposed to happen" >] + (str"The code which adds destructor hints broke;" ++ spc () ++ + str"this is not supposed to happen") let export_dd x = Some x -- cgit v1.2.3