diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-13 09:03:13 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-13 09:03:13 +0000 |
| commit | 78d1c75322684eaa7e0ef753ee56d9c6140ec830 (patch) | |
| tree | 3ec7474493dc988732fdc9fe9d637b8de8279798 /tactics/dhyp.ml | |
| parent | f813d54ada801c2162491267c3b236ad181ee5a3 (diff) | |
compat ocaml 3.03
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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:<Inversion $0>>]. + (:tactic:<Inversion $0>). Then, the tactic is used like this: @@ -91,7 +91,7 @@ hypothesis H. Similarly for the conclusion : -Hint Destruct Conclusion equal_zero (? = ?) 1 [<:tactic:<Reflexivity>>]. +Hint Destruct Conclusion equal_zero (? = ?) 1 (:tactic:<Reflexivity>). 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:<Inversion $0>>]. + (:tactic:<Inversion $0>). 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 |