Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 9 deletions

diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index bc876692d..5ea76696a 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -8,15 +8,18 @@
 
 (*i      $Id$       i*)
 
-Require Rbasic_fun.
+Require Import Rbasic_fun.
 
-Recursive Tactic Definition SplitAbs :=
-  Match Context With
-    | [ |- [(case_Rabsolu ?1)] ] -> 
-         Case (case_Rabsolu ?1); Try SplitAbs.
+Ltac split_case_Rabs :=
+  match goal with
+  |  |- context [(Rcase_abs ?X1)] =>
+      case (Rcase_abs X1); try split_case_Rabs
+  end.
 
 
-Recursive Tactic Definition SplitAbsolu :=
-  Match Context With
-    | [ id:[(Rabsolu ?)] |- ? ] -> Generalize id; Clear id;Try SplitAbsolu
-    | [ |- [(Rabsolu ?1)] ] ->  Unfold Rabsolu; Try SplitAbs;Intros.
+Ltac split_Rabs :=
+  match goal with
+  | id:context [(Rabs _)] |- _ => generalize id; clear id; try split_Rabs
+  |  |- context [(Rabs ?X1)] =>
+      unfold Rabs in |- *; try split_case_Rabs; intros
+  end.
\ No newline at end of file